abstract ;;Quote: event-driven state-machine programming (ESP) for programmable devices; generates a C program and SPIN model; 90% fewer lines of code, low overhead

312 ;;Quote: synchronous communication of immutable objects simplifies reasoning about message ordering; more efficient and easier to verify than buffered channels

313 ;;Quote: in ESP, memory safety is a local property of each process; reference counting of link/unlink; communicates immutable, acyclic objects; easily verified by SPIN

315 ;;Quote: SPIN--on-the-fly model checker; partial search with bit-state hashing and simulation mode

315+;;Quote: SPIN's simulation mode finds the most bugs; random choice at each turn; users rarely find rare bugs

316 ;;Quote: used SPIN to develop a retransmission protocol; 65 lines test code, all errors identified, 1/5 the development time

316 ;;Quote: ESP uses whole program analysis to generate code for event-driven state-machines; independent processes with context switch

316+;;Quote: an ESP context switch only saves the program counter; no stack needed for a state machine

317 ;;Quote: ESP uses a bit-mask of blocked channels per process; to check for a writer, collocate multiple processes on an integer

317 ;;Quote: increment reference count instead of sending deep copies over a channel; requires immutable objects

318 ;;Quote: ESP for efficient, device implementations of concurrent programming; other languages support concurrency but not as efficiently