The following technical report is available from
http://aib.informatik.rwth-aachen.de:
IC3 Software Model Checking
Tim Felix Lange
AIB 2019-02
In times where computers become ever smaller and more powerful and software becomes more complex and advances even deeper into every aspect of our lives, the risk of software misbehaviour and the resulting damage grows dramatically. In order to prevent such erroneous behaviour model checking, a formal verification technique for determining functional properties of information and communication systems, has proven to be highly useful.
For proving mathematical properties, one of the first methods to be taught in schools is induction. With the concept of proving a concrete induction base and a general induction step it is considered a very simple and intuitive, yet powerful proof method. However, for difficult properties finding an inductive formulation can be an extremely hard task. When humans try to solve this problem, they naturally produce a set of smaller, simple lemmas that together imply the desired property. Each of these lemmas holds relative to some subset of previously established lemmas by invoking the knowledge to prove the new lemma.
This incremental approach to proving complex properties using sets of small inductive lemmas was first applied to model checking of hardware systems in the IC3 algorithm and has proven to outperform all known approaches to hardware model checking.
This thesis aims at applying the principles of incremental, inductive verification laid by the IC3 algorithm to software model checking for industrial control software with special attention to the control-flow induced by the program under consideration. For this purpose, basic concepts are introduced and an in-depth explanation of the IC3 algorithm and its different building blocks (search phase, generalization and propagation) is given. Based on these prerequisites the novel IC3CFA algorithm is presented. In this algorithm, the control-flow of the program is explicitly modelled as an automaton, while the variable valuations are handled symbolically, thus using the best of both worlds. Following the search phase of IC3CFA, solutions for applying generalization to IC3CFA are presented and problems arising with propagation are discussed. Finally, the performance of the IC3CFA algorithm and all proposed improvements is extensively evaluated on a set of well-recognised benchmarks. To set these results into a relation, a comparison with other available IC3 software model checking implementations concludes this thesis and underlines the strong potential of the IC3CFA model checking algorithm.
