Proving safety with trace automata and bounded model checking
Loop under-approximation enriches C programs with additional branches that represent the effect of a (limited) range of loop iterations. While this technique can speed up bug detection significantly, it introduces redundant execution traces which may complicate the verification of the program. This...
| Autors principals: | , , |
|---|---|
| Altres autors: | |
| Format: | Conference item |
| Publicat: |
Springer
2015
|
| _version_ | 1826262693331337216 |
|---|---|
| author | Kroening, D Lewis, M Weissenbacher, G |
| author2 | Bjørner, N |
| author_facet | Bjørner, N Kroening, D Lewis, M Weissenbacher, G |
| author_sort | Kroening, D |
| collection | OXFORD |
| description | Loop under-approximation enriches C programs with additional branches that represent the effect of a (limited) range of loop iterations. While this technique can speed up bug detection significantly, it introduces redundant execution traces which may complicate the verification of the program. This holds particularly true for tools based on Bounded Model Checking, which incorporate simplistic heuristics to determine whether all feasible iterations of a loop have been considered. We present a technique that uses trace automata to eliminate redundant executions after performing loop acceleration. The method reduces the diameter of the program under analysis, which is in certain cases sufficient to allow a safety proof using Bounded Model Checking. Our transformation is precise–it does not introduce false positives, nor does it mask any errors. We have implemented the analysis as a source-to-source transformation, and present experimental results showing the applicability of the technique. |
| first_indexed | 2024-03-06T19:40:06Z |
| format | Conference item |
| id | oxford-uuid:205f3ffe-a2e1-4cec-9f1e-588f0b3c7277 |
| institution | University of Oxford |
| last_indexed | 2024-03-06T19:40:06Z |
| publishDate | 2015 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:205f3ffe-a2e1-4cec-9f1e-588f0b3c72772022-03-26T11:27:12ZProving safety with trace automata and bounded model checkingConference itemhttp://purl.org/coar/resource_type/c_5794uuid:205f3ffe-a2e1-4cec-9f1e-588f0b3c7277Symplectic Elements at OxfordSpringer2015Kroening, DLewis, MWeissenbacher, GBjørner, NBoer, FLoop under-approximation enriches C programs with additional branches that represent the effect of a (limited) range of loop iterations. While this technique can speed up bug detection significantly, it introduces redundant execution traces which may complicate the verification of the program. This holds particularly true for tools based on Bounded Model Checking, which incorporate simplistic heuristics to determine whether all feasible iterations of a loop have been considered. We present a technique that uses trace automata to eliminate redundant executions after performing loop acceleration. The method reduces the diameter of the program under analysis, which is in certain cases sufficient to allow a safety proof using Bounded Model Checking. Our transformation is precise–it does not introduce false positives, nor does it mask any errors. We have implemented the analysis as a source-to-source transformation, and present experimental results showing the applicability of the technique. |
| spellingShingle | Kroening, D Lewis, M Weissenbacher, G Proving safety with trace automata and bounded model checking |
| title | Proving safety with trace automata and bounded model checking |
| title_full | Proving safety with trace automata and bounded model checking |
| title_fullStr | Proving safety with trace automata and bounded model checking |
| title_full_unstemmed | Proving safety with trace automata and bounded model checking |
| title_short | Proving safety with trace automata and bounded model checking |
| title_sort | proving safety with trace automata and bounded model checking |
| work_keys_str_mv | AT kroeningd provingsafetywithtraceautomataandboundedmodelchecking AT lewism provingsafetywithtraceautomataandboundedmodelchecking AT weissenbacherg provingsafetywithtraceautomataandboundedmodelchecking |