Automated verification is an important step towards reliable software systems of the future. In this thesis, we concentrate on model-checking — an automated technique for deciding whether a system satisfies a temporal formula. We present techniques to address several major challenges facing adoption of model-checking as a practical verification technology.

To address the challenge of specifying correctness properties, we extend query-checking — a technique for discovering system’s properties based on user-supplied queries. We develop a language of queries based on Computation Tree Logic, and present an algorithm for it. The technique is implemented in TLQSOLVER. We report on analysis of a cruise control system, and demonstrate novel applications of query-checking.

The validity of model-checking is threatened by vacuous satisfaction — a case where the system passes the analysis for a wrong, and often trivial, reason. We build upon vacuity detection — a well-known sanity check. We argue that it is important to distinguish different levels of vacuity to provide a user with a better understanding of potential threats to the analysis. We present a more general definition of vacuity — mutual vacuity, that captures truth or falsity of a property together with its vacuity with respect to different subformulas and their occurrences.

To address the scalability challenge, we develop an abstraction technique that allows for verification and refutation of arbitrary temporal properties. Our main contributions are the systematic derivation of abstraction following Abstract Interpretation and a new characterization of the most precise abstract model for a given abstract domain.

To address the challenge of automatic analysis of software at the source code level, we present a new software model-checker YASM. YASM is based on a combination of the CounterExample Guided Abstraction Refinement with the abstraction technique presented in this thesis. The main distinguishing feature of YASM is support for both verification and refutation of properties of sequential C programs.

We address problems that occur at different stages of the model-checking process. The unifying theme is the use of the framework of multi-valued model-checking. The thesis also contributes to this framework by presenting a reduction technique between multi-valued and classical model-checking.