A Tool for Checking ANSI-C Programs

Abstract. We present a tool for the formal verification of ANSI-C programs using Bounded Model Checking (BMC). The emphasis is on usability: the tool supports almost all ANSI-C language features, including pointer constructs, dynamic memory allocation, recursion, and the float and double data types. From the perspective of the user, the verification is highly automated: the only input required is the BMC bound. The tool is integrated into a graphical user interface. This is essential for presenting long counterexample traces: the tool allows stepping through the trace in the same way a debugger allows stepping through a program.

• Type: Conference
• Year: 2004
• Where: TACAS
• Authors: Edmund M. Clarke, Daniel Kroening, Flavio Lerda
• Keywords: Algorithms, ANSI-C Language Features, Dynamic Memory Allocation, TACAS 2004, Tool