Integrating WS1S with PVS

Presented at CAV'00, Chicago, IL, July 2000. © Springer-Verlag.

---

Authors

Sam Owre and Harald Rueß

Abstract

We describe the integration of an automata-theoretic decision procedure of Weak Second-Order Monadic Logic (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}
}

---

Harald Ruess: ruess@csl.sri.com