SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Integrating WS1S with PVS
 by Sam Owre & Dr. Harald Rueß.

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.
BibTEX Entry
    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 = {}


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2024 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy