We address the problem of automatically establishing whether software is free of bugs. If it is bug-free, we aim to provide a formal proof. If it is not bug-free, we aim to provide a reproducible witness test that unveils the cause of the bug.
Context
The software embedded in a modern car controls many tasks at the same time: fuel injection, brakes, cruise control and navigation system. Ensuring that those concurrent tasks are performed correctly is of utmost importance: applying the brakes should disable cruise control, otherwise the driver cannot stop the car; setting a target location in the navigation system should not monopolise the system, because the computer also controls vital tasks such as braking. Beyond cars, we rely heavily on software that is used to control other embedded systems including in heart pacemakers, trains, aeroplanes and the electric power grid. We address the problem of automatically establishing whether software is free of concurrency bugs. If it is bug-free, we aim to provide a formal proof. If it is not bug-free, we aim to provide a reproducible witness test that unveils the cause of the bug.
Approach
We are actively researching and developing new methods and tools in a number of core automated formal methods areas. These areas include:
- Combining static analysis, model-checking and theorem proving
- Iterative on-demand trace refinement to eliminate false positives
- Modular analysis with context sensitive function summaries
- Verification of multi-threaded programs with partial order reduction and trace refinement
The figure gives an overview of the basis of our approach: a program P is abstracted into an automaton A that generates a language L(A), first abstraction being the control flow graph of the program. Then the abstraction refinement loop is iterated until we find a bug or declare the program bug-free. It may be the case that the loop never terminates. This is what is called refinement of trace abstractions as defined in Heizmann et al., SAS 2009.
Skink Tool -- SVCOMP 2017
The approach we propose has been implemented in a tool, Skink developed at Macquarie University. Skink analyses the LLVM-IR of programs. The IR can be generated using clang3.7.1-final. Skink is written in Scala. The front-end is written using our sbt-rats parser generator and our Kiama Scala library for language processing. The back-end SMT-solver is an abstraction over the SMTLIB standard. Our implementation is a Scala package MQ-Scala-SMTLIB.
- The SVCOMP 2017 version of Skink is skink-v2.0
Collaborations
Aalborg University, RWTH Aachen University, University of Freiburg, TU and LM Munich, Augsburg University, Magdeburg University, Germany
