Under-approximating loops in C programs for fast counterexample detection.
Form Methods Syst Des
; 47: 75-92, 2015.
Article
en En
| MEDLINE
| ID: mdl-26900259
ABSTRACT
Many software model checkers only detect counterexamples with deep loops after exploring numerous spurious and increasingly longer counterexamples. We propose a technique that aims at eliminating this weakness by constructing auxiliary paths that represent the effect of a range of loop iterations. Unlike acceleration, which captures the exact effect of arbitrarily many loop iterations, these auxiliary paths may under-approximate the behaviour of the loops. In return, the approximation is sound with respect to the bit-vector semantics of programs. Our approach supports arbitrary conditions and assignments to arrays in the loop body, but may as a result introduce quantified conditionals. To reduce the resulting performance penalty, we present two quantifier elimination techniques specially geared towards our application. Loop under-approximation can be combined with a broad range of verification techniques. We paired our techniques with lazy abstraction and bounded model checking, and evaluated the resulting tool on a number of buffer overflow benchmarks, demonstrating its ability to efficiently detect deep counterexamples in C programs that manipulate arrays.
Texto completo:
1
Banco de datos:
MEDLINE
Tipo de estudio:
Diagnostic_studies
Idioma:
En
Revista:
Form Methods Syst Des
Año:
2015
Tipo del documento:
Article
País de afiliación:
Reino Unido