| 
|
QuoteRef: shanAU9_1993
topics >
all references >
ThesaHelp:
ACM references m-z
ThesaHelp:
references sa-sz
Topic:
proving concurrent programs
Topic:
safety, liveness, and system properties
Reference
Shankar, A.U., "An introduction to assertional reasoning for concurrent systems", ACM Computing Surveys, 25, 3, pp. 225-262, September 1993. Google
abstract ;;Quote: model a concurrent system by state transitions and fairness requirements; use invariant and leads-to assertions and Hoare logic
226 ;;Quote: reason about concurrent systems using safety (nothing bad can happen) and progress (something good will happen) assertions
231 ;;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
236 ;;Quote: use invariants for safety properties, and leads-to and invariants for progress properties; includes every property for state-event sequences
ThesaHelp: ACM references m-z (280 items)
ThesaHelp: references sa-sz (237 items)
Topic: proving concurrent programs (37 items)
Topic: safety, liveness, and system properties (22 items)