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: 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: want to prove safety properties (e.g., no incorrect output) and liveness properties (e.g., termination of program) [»lampL_1980]

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

Quote: both termination and garbage collection satisfy safety (if marked, it is terminated/garbage) and liveness (will mark if terminated/garbage) [»telG1_1993]

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

Quote: an operation is kill-safe if it is atomic despite thread termination [»flatM6_2004]

Quote: how to extend a run-time system for kill-safe operations; only trusting the shared object

Quote: efficient type safety with CCured -- 3-87% time overhead, 1-284% space overhead; Purify and Valgrind are 5x to 130x slower [»necuGC5_2005]

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: a safety assertion is a behavioral invariant that is derivable from the specified modes and mode transitions; checked [»atleJM1_1993]

Quote: safety properties are closed under behavior prefixes and stuttering [»abadM1_1993]

Quote: used a model checker to verify safety assertions written in temporal logic; found subtle discrepancies [»atleJM1_1993]

Quote: safety is a quality of the system in which the software is used; it is not a quality of the software itself; reused software may be unsafe [»leveNG7_1993]

Quote: a liveness property includes continuations for every finite behavior [»abadM1_1993]

Quote: progress assertions are of the form 'P leads-to Q' where P and Q are predicates; no time bound is implied, but holds when system at rest [»shanAU9_1993]

Quote: to prove liveness properties such as termination need to prove safety properties such as monotonic decreases [»lampL_1980]

Quote: specify liveness axioms by temporal logic; uses box for henceforth and diamond for eventually; defines leads_to [»lampL1_1989]

Quote: automatic prover for liveness properties; extension of fair termination prover; handles large systems written in C [»cookB1_2007]

Quote: specify fair termination using Streett automata; fair non-termination iff either first Boolean succeeds only finitely often, or the second succeeds infinitely often [»cookB1_2007]

Quote: bug detectors for thread correctness, performance issue, security violation, usage bug, dropped exception, null pointer, open stream, unchecked return, unconditional wait [»hoveD12_2004]