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 postscript

Slides

gzipped postscript or postscript

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