Alexey Khoroshilov, Linux Verification Center, ISPRAS, Russia

Static analysis tools allow to check properties of a program looking at its source/binary code without executing the program. The main potential benefit of the approach is a possibility to check all possible execution paths at once without choosing test inputs and without a need to access physical hardware. As tools are maturing, static analysis is gaining adoption in software industry. Meanwhile, application of the tools in safety-critical domain has some specifics. Soundness of the analysis becomes a vital property as far as otherwise it is not possible to use the results of the analysis as an evidence in a certification process. Model checking is a very promising approach to code analysis in this respect.

The talk considers state of the art of open source model checkers for C programs on top of our experience of their usage within Linux Driver Verification program. The conventional characteristics such as time/memory efficiency and false positive rate are discussed as well as possible approaches to use them in safety critical domain.