Compile-Time Debugging of C Programs Working on Trees

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

  • Department of Computer Science
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, an 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 previous work that uses a similar technique to verify a simpler syntax manipulating only list structures. In that case, programs are translated into WS1S formulas. A naive generalization to recursive data-types determines an encoding in WS2S that leads to infeasible computations. To obtain a working tool, we have extended MONA to directly support recursive structures using an encoding that provides a necessary state-space factorization. This extension of MONA defines the new WSRT logic together with its decision procedure.
Original languageEnglish
Title of host publicationProgramming Languages and Systems : 9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000 Berlin, Germany, March 25 – April 2, 2000 Proceedings
EditorsGert Smolka
Number of pages16
PublisherSpringer
Publication year2000
Pages119-134
DOIs
Publication statusPublished - 2000
EventEuropean Symposium on Programming. ESOP 2000 - Berlin, Germany
Duration: 25 Mar 20002 Apr 2000
Conference number: 9

Conference

ConferenceEuropean Symposium on Programming. ESOP 2000
Nummer9
LandGermany
ByBerlin
Periode25/03/200002/04/2000
SeriesLecture Notes in Computer Science
Volume1782
ISSN0302-9743

See relations at Aarhus University Citationformats

ID: 3739656