From Refutation to Verification
John Rushby
Invited paper from
Formal Description Techniques and
Protocol Specification, Testing and Verification (FORTE XIII/PSTV XX),
pp. 369-374,
October 2000, Pisa, Italy. © Kluwer Academic Publishers.
Abstract
Model checking has won some industrial acceptance in debugging
designs. Theorem proving and formal verification are less
popular. An approach built around automated abstractions could
integrate theorem proving with model checking in an acceptable way and
provide a bridge between refutation and verification.
gzipped postscript,
or
plain postscript
or
pdf
or
crude ascii (for your Palm Pilot)
Slides
gzipped postscript,
or
plain postscript
or
pdf
or
crude ascii (for your Palm Pilot)
BibTeX Entry
@INPROCEEDINGS{Rushby00:Forte,
AUTHOR = {John Rushby},
TITLE = {From Refutation to Verification},
BOOKTITLE = {Formal Description Techniques and Protocol Specification,
Testing and Verification {FORTE XIII/PSTV XX 2000}},
EDITOR = {Tommaso Bolognesi and Diego Latella},
YEAR = 2000,
MONTH = oct,
PAGES = {369--374},
ADDRESS = {Pisa, Italy},
PUBLISHER = {Kluwer Academic Publishers},
URL = {http://www.csl.sri.com/~rushby/forte-pstv2000.html}
}
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page