Accelerating invariant generation
Acceleration is a technique for summarising loops by computing a closed-form representation of the loop behaviour. The closed form can be turned into an accelerator, which is a code snippet that skips over intermediate states of the loop to the end of the loop in a single step. Program analysers rel...
| Prif Awduron: | , , , , |
|---|---|
| Awduron Eraill: | |
| Fformat: | Conference item |
| Cyhoeddwyd: |
IEEE
2016
|
| _version_ | 1826299517394223104 |
|---|---|
| author | Madhukar, K Wachter, B Kroening, D Lewis, M Srivas, M |
| author2 | Kaivola, R |
| author_facet | Kaivola, R Madhukar, K Wachter, B Kroening, D Lewis, M Srivas, M |
| author_sort | Madhukar, K |
| collection | OXFORD |
| description | Acceleration is a technique for summarising loops by computing a closed-form representation of the loop behaviour. The closed form can be turned into an accelerator, which is a code snippet that skips over intermediate states of the loop to the end of the loop in a single step. Program analysers rely on invariant generation techniques to reason about loops. The state-of-the-art invariant generation techniques, in practice, often struggle to find concise loop invariants, and, instead, degrade into unrolling loops, which is ineffective for non-trivial programs. In this paper, we evaluate experimentally whether loop accelerators enable existing program analysis algorithm to discover loop invariants more reliably and more efficiently. This paper is the first comprehensive study on the synergies between acceleration and invariant generation. We report our experience with a collection of safe and unsafe programs drawn from the Software Verification Competition and the literature. |
| first_indexed | 2024-03-07T05:03:08Z |
| format | Conference item |
| id | oxford-uuid:d8ffa6ee-3b33-4e2c-bc14-770d4aca94e4 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T05:03:08Z |
| publishDate | 2016 |
| publisher | IEEE |
| record_format | dspace |
| spelling | oxford-uuid:d8ffa6ee-3b33-4e2c-bc14-770d4aca94e42022-03-27T08:52:53ZAccelerating invariant generationConference itemhttp://purl.org/coar/resource_type/c_5794uuid:d8ffa6ee-3b33-4e2c-bc14-770d4aca94e4Symplectic Elements at OxfordIEEE2016Madhukar, KWachter, BKroening, DLewis, MSrivas, MKaivola, RWahl, TAcceleration is a technique for summarising loops by computing a closed-form representation of the loop behaviour. The closed form can be turned into an accelerator, which is a code snippet that skips over intermediate states of the loop to the end of the loop in a single step. Program analysers rely on invariant generation techniques to reason about loops. The state-of-the-art invariant generation techniques, in practice, often struggle to find concise loop invariants, and, instead, degrade into unrolling loops, which is ineffective for non-trivial programs. In this paper, we evaluate experimentally whether loop accelerators enable existing program analysis algorithm to discover loop invariants more reliably and more efficiently. This paper is the first comprehensive study on the synergies between acceleration and invariant generation. We report our experience with a collection of safe and unsafe programs drawn from the Software Verification Competition and the literature. |
| spellingShingle | Madhukar, K Wachter, B Kroening, D Lewis, M Srivas, M Accelerating invariant generation |
| title | Accelerating invariant generation |
| title_full | Accelerating invariant generation |
| title_fullStr | Accelerating invariant generation |
| title_full_unstemmed | Accelerating invariant generation |
| title_short | Accelerating invariant generation |
| title_sort | accelerating invariant generation |
| work_keys_str_mv | AT madhukark acceleratinginvariantgeneration AT wachterb acceleratinginvariantgeneration AT kroeningd acceleratinginvariantgeneration AT lewism acceleratinginvariantgeneration AT srivasm acceleratinginvariantgeneration |