Computer Science Department
School of Computer Science, Carnegie Mellon University
Model Checking and Theorem Proving:
Many new methodologies have been proposed to make the two techniques work in ensemble. Observing such a wide variety of methodologies, one may even question the mere possibility of finding a universal technique that would combine model checking and theorem proving. Instead, it seems more practical to expand the collection of these problem-specific methodologies.
The development of new methodologies is usually an iterative experimental process in which researchers implement their ideas in a prototype tool and run several verification examples in it. The experiments provide the necessary feedback for refining the methodology and generalizing it to handle wider class of examples, or give hints on how to tune the technique to specific applications.
Since the methodologies often use both model checking and theorem proving techniques, implementing new tools becomes the main bottleneck in their development. In this work, we provide a new unified framework that includes both model checking and theorem proving, and is designed for fast prototyping or manual but computer-assisted testing of new verification methodologies. The tool SyMP (Symbolic Model Prover) implements this methodology in a theorem prover-like environment. Moreover, the tool is in fact a programmer's kit for generating new, possibly highly specialized, theorem provers. It provides a base for the development of new tools for emerging methodologies and reduces the implementation time. The architecture of the tool and the theory behind it help organizing the new methodologies in a systematic and extensible way.