New Directions in Symbolic
Model Checking

By Julien D'Orso
December 2003
Uppsala University Press
ISBN: 91-554-5781-9
130 pages, 6 ½" x 9 ½"
$49.50 Paper Original

---

This is a Ph.D. dissertation. In today's computer engineering, requirements for generally high reliability have pushed the notion of testing to its limits. Many disciplines are moving, or have already moved, to more formal methods to ensure correctness. This is done by comparing the behavior of the system as it is implemented against a set of requirements. The ultimate goal is to create methods and tools that are able to perform this kind of verification automatically: this is called Model Checking. Although the notion of model checking has existed for two decades, adoption by the industry has been hampered by its poor applicability to complex systems. During the 90s, researchers have introduced an approach to cope with large (even infinite) state spaces: Symbolic Model Checking. The key notion is to represent large (possibly infinite) sets of states by a small formula (as opposed to enumerating all members). In this thesis, symbolic methods are applied to the following different types of systems: Parameterized systems, Games on Infinite Structures, and Probabilistic Systems.

Computer Science
Uppsala Dissertations from the Faculty of Science & Technology, No. 50

Return to Coronet Books main page