Under-approximating loops in C programs for fast counterexample detection
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. U...
| Main Authors: | , , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
Springer Verlag
2015
|
| _version_ | 1797059464227979264 |
|---|---|
| author | Kroening, D Lewis, M Weissenbacher, G |
| author_facet | Kroening, D Lewis, M Weissenbacher, G |
| author_sort | Kroening, D |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-06T20:04:36Z |
| format | Journal article |
| id | oxford-uuid:28831064-29d6-4edd-b689-df8069b440c6 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T20:04:36Z |
| publishDate | 2015 |
| publisher | Springer Verlag |
| record_format | dspace |
| spelling | oxford-uuid:28831064-29d6-4edd-b689-df8069b440c62022-03-26T12:13:15ZUnder-approximating loops in C programs for fast counterexample detectionJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:28831064-29d6-4edd-b689-df8069b440c6EnglishSymplectic Elements at OxfordSpringer Verlag2015Kroening, DLewis, MWeissenbacher, GMany 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. |
| spellingShingle | Kroening, D Lewis, M Weissenbacher, G Under-approximating loops in C programs for fast counterexample detection |
| title | Under-approximating loops in C programs for fast counterexample detection |
| title_full | Under-approximating loops in C programs for fast counterexample detection |
| title_fullStr | Under-approximating loops in C programs for fast counterexample detection |
| title_full_unstemmed | Under-approximating loops in C programs for fast counterexample detection |
| title_short | Under-approximating loops in C programs for fast counterexample detection |
| title_sort | under approximating loops in c programs for fast counterexample detection |
| work_keys_str_mv | AT kroeningd underapproximatingloopsincprogramsforfastcounterexampledetection AT lewism underapproximatingloopsincprogramsforfastcounterexampledetection AT weissenbacherg underapproximatingloopsincprogramsforfastcounterexampledetection |