IC3 Software Model Checking
Tim Felix Lange
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.