Wasser, Nathan ; Bubel, Richard ; Hähnle, Reiner (2015)
Array Abstraction with Symbolic Pivots.
Report, Bibliographie
Kurzbeschreibung (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.
| Typ des Eintrags: | Report |
|---|---|
| Erschienen: | 2015 |
| Autor(en): | Wasser, Nathan ; Bubel, Richard ; Hähnle, Reiner |
| Art des Eintrags: | Bibliographie |
| Titel: | Array Abstraction with Symbolic Pivots |
| Sprache: | Deutsch |
| Publikationsjahr: | August 2015 |
| Zugehörige Links: | |
| Kurzbeschreibung (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. |
| Freie Schlagworte: | loop invariant generation, program verification, abstract interpretation, array abstraction |
| ID-Nummer: | TUD-CS-2015-1213 |
| Fachbereich(e)/-gebiet(e): | 20 Fachbereich Informatik 20 Fachbereich Informatik > Formal Methods in System Engineering 20 Fachbereich Informatik > Software Engineering |
| Hinterlegungsdatum: | 31 Dez 2016 10:40 |
| Letzte Änderung: | 03 Jun 2018 21:31 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum