************************************************************************ ** * Einladung * * * Informatik-Oberseminar * * ************************************************************************

Zeit: Freitag, 5. Oktober 2018, 10:00 Uhr Ort: Gebäude E2, B-IT-Seminarraum 5053.1, Ahornstr. 55

Referent: Herr Tim Lange, M.Sc.

Titel: IC3 Software Model Checking

Abstract:

Many real-world systems are becoming ever smaller in size and more powerful, such that software becomes more complex. The risk of ubiquitous softwares' misbehaviour and the resulting damage therefore 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, finding an inductive formulation for difficult properties 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 talk 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. Finally, the performance of the IC3CFA algorithm and all proposed improvements is extensively evaluated on a set of well-recognised benchmarks.

Es laden ein: Die Dozenten der Informatik