Quote: reason about concurrent systems using safety (nothing bad can happen) and progress (something good will happen) assertions [»shanAU9_1993]

Quote: prove that each component behaves correctly in isolation when its environment is correct; then proof rule for composition under safety and liveness conditions [»abadM1_1993]

Quote: for concurrent programming, prove that bad things can't happen and good things do; i.e., an expression of the program's variables; avoids process interleavings [»schnFB4_1998]

Quote: type systems say nothing about concurrency or dynamics; e.g., that initialize happens first, or x() must be invoked every 10 ms [»leeEA9_2000]

Quote: desired properties for state machines--absence of deadlock, completeness, and liveness; catch basic flaws and unwarranted assumptions [»holzGJ5_1999]

Quote: liveness is much harder to prove than safety, yet it is just as important; must prove that g() terminates to prove that h() occurs in f;g;h [»cookB1_2007]

Quote: algorithm for mutual exclusion of readers and writers; minimize delay of readers or writers; based on P, V, and active counts [»courPJ10_1971]

Quote: for reasoning about concurrent programs, replace weakest precondition and strongest postcondition with weakest and strongest invariants [»lampL7_1990]

Quote: use invariants for safety properties, and leads-to and invariants for progress properties; includes every property for state-event sequences [»shanAU9_1993]

Quote: extend Hoare's assertions to concurrent programs by pre-conditions holding until termination of unit; equivalent for atomic actions [»lampL_1980]

Quote: model a concurrent system by state transitions and fairness requirements; use invariant and leads-to assertions and Hoare logic [»shanAU9_1993]

Quote: when does a property hold whether or not a statement is interruptible? [»liptRJ12_1975]

Quote: a right mover is a "release" [V] that can move later in an interleaving; a left mover is a "seize" [P] that can move earlier [»liptRJ12_1975]

Quote: for proofs, can treat a sequence as atomic if it consists of right movers (V) followed by left movers (P) [»liptRJ12_1975]

Quote: validate Eventrons at run-time before scheduling; no allocation or pointer modification; creates a data-specific call graph [»spooD6_2006]

Quote: occam has a formal semantics; used an interactive transformation system to prove that an occam program satisfied the IEEE floating point standard [»mayD_1987]

Quote: use a formal specification for synchronization primitives on a multiprocessor; otherwise difficult questions about their precise semantics [»birrAD_1991a]

Quote: formal specification of Modula-3 threads for safety properties and termination; ignores liveness [»birrAD_1991a]

Quote: programmers and implementers use the formal specification of Modula-3 threads [»birrAD_1991a]

Quote: an untrained user found an error in the formal specification of Modula-3 threads; another error was missed for a year

Quote: Sing# has formal message passing semantics; all processes run in one virtual address space without overwriting data; avoids kernel traps and context switches [»taneAS5_2006]

Quote: Sing# sends strongly typed messages over bidirectional channels; a state machine defines the channel's protocol [»taneAS5_2006]

Quote: the dining philosophers problem demonstrates the constructive approach to multiprogramming correctness [»dijkEW2_1971]

Quote: introduce the intermediate state, 'hungry', to solve the dining philosophers problem

Quote: used detailed, hierarchical proofs since theorems about concurrent system specifications are difficult to get right [»abadM1_1993]

Quote: a concurrent language needs simple constructs that guarantee determinism; usually not true of message communication systems [»chanKM7_1980]

Quote: verify atomicity using Lipton's right and left movers; lock acquisition moves to the right while lock release moves left; atomic if acquisition and release move to start and end respectively [»flanC6_2003]

Quote: a specification is realizable iff the system has a winning strategy; i.e., the system wins under all legal environment behaviors [»abadM1_1993]

Quote: process autonomy--each component of a distributed program should be designed and proved separately; can not name other processes [»chanKM7_1980]

Quote: efficient search technique for detecting deadlocks and assertion violations in concurrent programs [»godeP1_1997]

Quote: transition-axiom method for proving concurrent systems combines abstract programs and temporal logic; rules for implementation and composition [»abadM1_1993]

Quote: specify atomic operations for concurrent programs by angle brackets, e.g., ' := ' [»lampL_1980]

Quote: in proofs of concurrent programs need to introduce value variables for intermediate results [»lampL_1980]

Quote: specify a non-atomic, concurrent procedure with a predicate that defines the allowable sequences of atomic actions

Quote: data-driven programs simplify correctness proofs, use data streams instead of elements; queuing-network analysis, and microcomputer networks [»dennPJ_1980]

Quote: threaded programs are extremely difficult to prove equivalent; due to the enormous number of possible interleavings [»leeEA5_2006]

Quote: sequential execution is function composition; a neat, simple model with deterministic results [»leeEA5_2006]