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