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.
2003
Proceedings - 1st International Conference on Software Engineering and Formal Methods, SEFM 2003
10662 LOS VAQUEROS CIRCLE, PO BOX 3014, LOS ALAMITOS, CA 90720-1264 USA
Institute of Electrical and Electronics Engineers Inc.
0-7695-1949-0
Deharbe, D.; Ranise, S.
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].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/333090
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 37
  • ???jsp.display-item.citation.isi??? 6
  • OpenAlex ND
social impact