Model Checking and Beyond

University Of Texas At Austin, Austin TX

Investigators

Abstract

There is a chronic need for more effective methods of designing correct and robust computer software as well as hardware. A method called "Model Checking" has been developed, providing an algorithmic means for establishing correctness of nominally finite state programs. Computer manufacturers such as IBM, Intel, and Motorola are finding model checking useful for verifying computer hardware circuits of moderate size. However, further research is required before model checking can be applied successfully to large hardware designs and to software. Software is more difficult to construct and verify than hardware due to its less uniform organization and sheer scale. Techniques to cope with irregular organization based on partial order and asymmetry reduction facilitating application of model checking to large software systems will be investigated. Other central topics of investigation include: new and improved basic techniques, including abstractions, algorithms, and data structures, for more efficient model checking; integration of model checking with other program design methods; automatic program synthesis via model checking; and the feasibility of extending the dichotomous (correct/incorrect) framework of conventional model checking using richer program robustness notions.