Model checking and test generation: towards a combined approach to software verification

Ensuring the correctness of safety-critical systems is a key aspect of the development process. Various approaches exist to find software bugs: (1) model checking examines the mathematical model of the software and proves the logical correctness, while (2) testing is an efficient and practical technique to find bugs. Model checking is a computationally expensive task, as it explores all the possible states of the software, and despite the technological advances of the last decade, software that cannot be formally verified still exists. On the other hand, testing is computationally cheaper than model checking, and widely used by the industry, but providing an efficient test suite for a given program is still under heavy research. The goal of my work is to combine model checking and testing to exploit the advantages of both approaches. I introduce a new algorithm that uses an abstraction-based model checking technique to explore the behavior of the software. In case the model checking algorithm proves the properties of the software, the procedure terminates. If the algorithm can not reach a conclusion, test generation is applied, exploiting the information gathered during state space traversal of model checking.