Static Analysis for Model-Checking Assembly Code


Jörg Bauer

Title Static Analysis for Model-Checking Assembly Code
When 16.07.2009
Where Lecture Room Informatik 7
Abstract [mc]square is a model checker for microcontroller assembly code that is being developed at the Embedded Software Laboratory of the RWTH Aachen University. An advantage of model checking assembly code is that all bugs in a program including compiler errors, reentrance problems, etc. can be found. A drawback, however, is that the state-explosion problem tends to be worse than for higher-level models due to the detailed representation of the underlying hardware. Using static analysis is one particular approach to tackle the state explosion.

In the context of [mc]square, we use static analysis for two purposes. First of all, it is used to statically generate abstractions of the program under scrutiny in order to obtain state-space reductions. Furthermore, static analysis can automatically detect certain defects in programs without the need to execute the time-consuming model-checking process. Static analysis for assembly code, however, significantly differs from static analysis for high-level languages. Features of the microcontroller hardware such as interrupts and the runtime stack have to be taken into account. Moreover, different analyses are interdependent and often the results of one analysis influence the results of other analyses. In this talk, we present a framework for static analysis on assembly-code level, which handles these challenges.