
Integrating WS1S with PVS
by Sam Owre & Dr. Harald Rueß.
Lecture Notes in Computer Science, Volume 1855. From ComputerAided Verification, CAV '2000. Edited by E. A. Emerson and A. P. Sistla. SpringerVerlag, Chicago, IL. July, 2000. Pages 548–551.
Abstract
We describe the integration of an automatatheoretic decision procedure of WS1S, based on
the MONA tool, with the PVS theorem prover. We give an overview of a new PVS tactic
that combinates abstraction, theorem proving, and the construction of automata for deciding
an interesting fragment of the PVS specification language. This fragment is rich enough to
encode many interesting theories such as Presburger arithmetic, lossy queues, regular
expressions, a restricted linear temporal logic, or fixedsized bitvectors. The integration of
WS1S decision procedures enriches PVS by providing new automated proving capabilities,
an alternative approach for combining decision procedures, and a method for generating
counterexamples from failed proof attempts. On the other hand, this integration provides an
appealing frontend and input language for the MONA tool, and permits using
automatatheoretic decision procedures in conjunction with both traditional theorem proving
techniques and specialized symbolic analysis like abstraction.
BibT_{E}X Entry
@inproceedings{Owre&Ruess00:CAV,
AUTHOR = {Sam Owre and Harald Rue\ss},
TITLE = {Integrating {WS1S} with {PVS}},
BOOKTITLE = {ComputerAided Verification, {CAV} '2000},
YEAR = {2000},
EDITOR = {{E.} {A.} Emerson and {A.} {P.} Sistla},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1855},
PAGES = {548551},
ADDRESS = {Chicago, {IL}},
MONTH = {jul},
PUBLISHER = {SpringerVerlag},
URL = {http://www.csl.sri.com/papers/cav00/}
}
Files

