Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification
John Rushby
Presented at
CAV'00, Chicago, IL, July 2000.
© Springer-Verlag. The final version will be available at
the Springer LNCS site
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, but derives from different
intuitions. 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.
gzipped postscript,
or
plain postscript
or
pdf
or
crude ascii (for your Palm Pilot)
Slides
gzipped postscript
or
postscript
or
pdf
or
crude ascii (for your Palm Pilot)
PVS Files
PVS dump file,
BibTeX Entry
@inproceedings{Rushby00:CAV,
TITLE = {Verification Diagrams Revisited: Disjunctive Invariants
for Easy Verification},
AUTHOR = {John Rushby},
BOOKTITLE = {Computer-Aided Verification, CAV '2000},
EDITOR = {E. A. Emerson and A. P. Sistla},
PAGES = {508--520},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1855,
MONTH = jul,
YEAR = 2000,
ADDRESS = {Chicago, IL}
}
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page