TU Darmstadt / ULB / TUbiblio

Array Abstraction with Symbolic Pivots

Wasser, Nathan and Bubel, Richard and Hähnle, Reiner (2015):
Array Abstraction with Symbolic Pivots.
[Report]

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 and Bubel, Richard and Hähnle, Reiner
Title: Array Abstraction with Symbolic Pivots
Language: German
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
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
Identification Number: TUD-CS-2015-1213
Related URLs:
Export:
Suche nach Titel in: TUfind oder in Google
Send an inquiry Send an inquiry

Options (only for editors)

View Item View Item