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.
Light-weight theorem proving for debugging and verifying units of code / Deharbe, D.; Ranise, S.. - (2003), pp. 220-228. (Intervento presentato al convegno 1st International Conference on Software Engineering and Formal Methods, SEFM 2003 tenutosi a aus nel 2003) [10.1109/SEFM.2003.1236224].
Light-weight theorem proving for debugging and verifying units of code
Ranise S.
2003-01-01
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione