Model checking and theorem proving: A unified framework  Posted on:20030108  Degree:Ph.D  Type:Dissertation  University:Carnegie Mellon University  Candidate:Berezin, Sergey  Full Text:PDF  GTID:1468390011985401  Subject:Computer Science  Abstract/Summary:   The neverending growth of the complexity of modern hardware and software systems requires more and more sophisticated methods of verification. The state space explosion problem leaves little hope for automatic finitestate verification techniques like model checking to remain practical, especially when designs become parameterized. The use of theorem proving techniques is inevitable to cope with the new verification challenges. “Pure” theorem proving, on the other hand, can also be quite tedious and impractical for complex designs. Ideally, one would like to find an efficient combination of model checking and theorem proving, and the quest for such a combination has long been one of the major challenges in the field of formal verification.; 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 problemspecific 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 of tools or manual but computerassisted testing of new verification methodologies. The tool SyMP (Symbolic Model Prover) implements this framework in a theorem proverlike 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.  Keywords/Search Tags:  Theorem proving, New, Methodologies, Verification, Tool   Related items 
 
