| 
|
QuoteRef: cookB1_2007
Topic:
safety, liveness, and system properties
Topic:
proving concurrent programs
Group:
program proving
Reference
Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., Vardi, M.Y., "Proving that programs eventually do something good", Conference Record of POPL 2007: The 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Nice, France, January 2007, pp. 55-61. Google
265 ;;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
265 ;;Quote: automatic prover for liveness properties; extension of fair termination prover; handles large systems written in C
266 ;;Quote: specify fair termination using Streett automata; fair non-termination iff either first Boolean succeeds only finitely often, or the second succeeds infinitely often
267 ;;Quote: prove that program satisfies a specification by proving that a combined program never calls the error function; insert the specification whereever its pattern is triggered
Topic: safety, liveness, and system properties (22 items)
Topic: proving concurrent programs (37 items)
Group: program proving (10 topics, 311 quotes)