Light-weight theorem proving for debugging and verifying units of code
- 1 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
Software bugs are very difficult to detect even in small units of code. Several techniques to debug or prove correct such units are based on the generation of a set of formulae whose unsatisfiability reveals the presence of an error. These techniques assume the availability of a theorem prover capable of automatically discharging the resulting proof obligations. Building such a tool is a difficult, long, and error-prone activity. In this paper, we describe techniques to build provers which are highly automatic and flexible by combining state-of-the-art superposition theorem provers and BDDs. We report experimental results on formulae extracted from the debugging of C functions manipulating pointers showing that an implementation of our techniques can discharge proof obligations which cannot be handled by Simplify (the theorem prover used in the ESC/Java tool) and perform much better on others.Keywords
This publication has 17 references indexed in Scilit:
- A rewriting approach to satisfiability proceduresInformation and Computation, 2003
- Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer ProgramsElectronic Notes in Theoretical Computer Science, 2003
- A proof of burns N-process mutual exclusion algorithm using abstractionPublished by Springer Nature ,1998
- Introduction to the OBDD algorithm for the ATP communityJournal of Automated Reasoning, 1994
- Theorem-proving with resolution and superpositionJournal of Symbolic Computation, 1991
- Simplification by Cooperating Decision ProceduresACM Transactions on Programming Languages and Systems, 1979
- Conditional Expressions with Equality TestsJournal of the ACM, 1978
- Assignment Commands with Array ReferencesJournal of the ACM, 1978
- Symbolic execution and program testingCommunications of the ACM, 1976
- A Basis for a Mathematical Theory of Computation)Published by Elsevier ,1963