Wasser, Nathan ; Bubel, Richard ; Hähnle, Reiner (2015)
Array Abstraction with Symbolic Pivots.
Report, Bibliographie
Abstract
In this paper we present a novel approach to automatically generate invariants for loops manipulating arrays. The intention is to achieve deductive program verification without the need for user-specified loop invariants. Many loops iterate and manipulate collections. Finding useful, i.e., sufficiently precise invariants for those loops is a challenging task, in particular, if the iteration order is complex. Our approach partitions an array and provides an abstraction for each of these partitions. Symbolic pivot elements are used to compute the partitions. In addition we integrate a faithful and precise program logic for sequential (Java) programs with abstract interpretation using an extensible multi-layered framework to compute array invariants. The presented approach has been implemented.
| Item Type: | Report |
|---|---|
| Erschienen: | 2015 |
| Creators: | Wasser, Nathan ; Bubel, Richard ; Hähnle, Reiner |
| Type of entry: | Bibliographie |
| Title: | Array Abstraction with Symbolic Pivots |
| Language: | German |
| Date: | August 2015 |
| Corresponding Links: | |
| Abstract: | In this paper we present a novel approach to automatically generate invariants for loops manipulating arrays. The intention is to achieve deductive program verification without the need for user-specified loop invariants. Many loops iterate and manipulate collections. Finding useful, i.e., sufficiently precise invariants for those loops is a challenging task, in particular, if the iteration order is complex. Our approach partitions an array and provides an abstraction for each of these partitions. Symbolic pivot elements are used to compute the partitions. In addition we integrate a faithful and precise program logic for sequential (Java) programs with abstract interpretation using an extensible multi-layered framework to compute array invariants. The presented approach has been implemented. |
| Uncontrolled Keywords: | loop invariant generation, program verification, abstract interpretation, array abstraction |
| Identification Number: | TUD-CS-2015-1213 |
| Divisions: | 20 Department of Computer Science 20 Department of Computer Science > Formal Methods in System Engineering 20 Department of Computer Science > Software Engineering |
| Date Deposited: | 31 Dec 2016 10:40 |
| Last Modified: | 03 Jun 2018 21:31 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Send an inquiry |
Options (only for editors)
 |
Show editorial Details |
Drucken
Impressum