Model checking LTL properties over ANSI-C programs with bounded traces

Аннотация

Context-bounded model checking has been used successfully to verify safety properties in multi-threaded systems automatically, even if they are implemented in low-level programming languages such as C. In this paper, we describe and experiment with an approach to extend context-bounded software model checking to safety and liveness properties expressed in linear-time temporal logic (LTL). Our approach checks the actual C program, rather than an extracted abstract model. It converts the LTL formulas into Büchi automata for the corresponding never claims and then further into C monitor threads that are interleaved with the execution of the program under analysis.