Integrating WS1S with PVS
Authors
Sam Owre and Harald Rueß
Abstract
We describe the integration of an automata-theoretic 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 fixed-sized
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 automata-theoretic decision procedures in conjunction with both
traditional theorem proving techniques and specialized symbolic analysis
like abstraction.
gzipped postscript
or
postscript
BibTeX Entry
@inproceedings{Owre&Ruess00:CAV,
TITLE = {Integrating {WS1S} with {PVS}},
AUTHOR = {Sam Owre and Harald Rue{\ss}},
BOOKTITLE = {Computer-Aided Verification, CAV '2000},
EDITOR = {E. A. Emerson and A. P. Sistla},
PAGES = {548--551},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1855,
MONTH = jul,
YEAR = 2000,
ADDRESS = {Chicago, IL}
}
Sam Owre:
owre@csl.sri.com