Sciweavers

Share
ESOP
2000
Springer

Compile-Time Debugging of C Programs Working on Trees

11 years 5 months ago
Compile-Time Debugging of C Programs Working on Trees
We exhibit a technique for automatically verifying the safety of simple C programs working on tree-shaped data structures. We do not consider the complete behavior of programs, but only attempt to verify that they respect the shape and integrity of the store. A verified program is guaranteed to preserve the tree-shapes of data structures, to avoid pointer errors such as NULL dereferences, leaking memory, and dangling references, and furthermore to satisfy assertions specified in a specialized store logic. A program is transformed into a single formula in WSRT, a novel extension of WS2S that is decided by the MONA tool. This technique is complete for loop-free code, but for loops and recursive functions we rely on Hoare-style invariants. A default well-formedness invariant is supplied and can be strengthened as needed by programmer annotations. If a program fails to verify, a counterexample in the form of an initial store that leads to an error is automatically generated. This extends p...
Jacob Elgaard, Anders Møller, Michael I. Sc
Added 24 Aug 2010
Updated 24 Aug 2010
Type Conference
Year 2000
Where ESOP
Authors Jacob Elgaard, Anders Møller, Michael I. Schwartzbach
Comments (0)
books