Formal Verification of McMillan's Compositional Assume-Guarantee Rule

John Rushby

Technical Report, September 2001


To illustrate some of the power and convenience of its specification language and theorem prover, we use the PVS formal verification system to verify the soundness of a proof rule for assume-guarantee reasoning due to Ken McMillan.

gzipped postscript, or plain postscript or PDF or crude ascii (for your Palm Pilot)

BibTeX Entry

	TITLE = {Formal Verification of {McMillan's} Compositional Assume-Guarantee Rule},
	AUTHOR = {John Rushby},
	ADDRESS = mp,
	MONTH = sep,
	YEAR = 2001

Having trouble reading our papers?
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page