Formal Verification of McMillan's Compositional
Assume-Guarantee Rule
John Rushby
Technical Report, September 2001
Abstract
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
@TECHREPORT{Rushby01:McMillan,
TITLE = {Formal Verification of {McMillan's} Compositional Assume-Guarantee Rule},
AUTHOR = {John Rushby},
INSTITUTION = csl,
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