SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification
 by Dr. John Rushby.

Abstract. I describe a systematic method for deductive verification of safety properties of concurrent programs. The method has much in common with the "verification diagrams" of Manna and Pnueli [17], but derives from different in tuitions. It is based on the idea of strengthening a putative safety property into a disjunction of "configurations" that can easily be proved to be inductive. Transitions among the configurations have a natural diagrammatic representation that conveys insight into the operation of the program. The method lends itself to mechanization and is illustrated using a simplified version of an example that had defeated previous attempts at deductive verification.


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2024 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy