Lecture Notes in Computer Science, Volume 1855.
From Computer-Aided Verification, CAV '2000.
Edited by E. A. Emerson and A. P. Sistla.
Springer-Verlag, Chicago, IL.
July, 2000.
Pages 548–551.

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.

@inproceedings{Owre&Ruess00:CAV,
    AUTHOR = {Sam Owre and Harald Rue\ss},
    TITLE = {Integrating {WS1S} with {PVS}},
    BOOKTITLE = {Computer-Aided Verification, {CAV} '2000},
    YEAR = {2000},
    EDITOR = {{E.} {A.} Emerson and {A.} {P.} Sistla},
    SERIES = {Lecture Notes in Computer Science},
    VOLUME = {1855},
    PAGES = {548--551},
    ADDRESS = {Chicago, {IL}},
    MONTH = {jul},
    PUBLISHER = {Springer-Verlag},
    URL = {http://www.csl.sri.com/papers/cav00/}
}

• cav00.pdf
• cav00.ps