Automata-based techniques for shape analysis

Ahmed Bouajjani

Abstract: We propose an
approach for the automatic analysis of programs with dynamic linked
structures using finite-state word/tree automata as representations for
(potentially infinite) sets of heap structures. A heap of a given
program is encoded as a word or a tree over an appropriate alphabet,
and each statement in the program is translated into a transducer (I/O
automaton) defining a transformation on the heap encodings. Then,
iterative reachability analysis is performed using automata techniques
in order to compute an upper-approximation of the set of all reachable
heap configurations. The reachability analysis uses abstractions on
automata representations (corresponding to finite index equivalence
relations on their state space) allowing to speed up the fixpoint
computation and to force termination. Automatic abstraction refinement
is applied by need based on conterexample analysis. The proposed
approach has been implemented and applied on various non trivial
examples of programs.

This is a joint work with Peter Habermehl, Pierre Moro, Adam Rogalewicz, and Tomas Vojnar.

This is a joint work with Peter Habermehl, Pierre Moro, Adam Rogalewicz, and Tomas Vojnar.

Can logic tame systems programs?

Cristiano Calcagno

Abstract: We report on our
experience on designing and implementing tools for automatic reasoning
about safety of systems programs using separation logic. We highlight
some of the fundamental obstacles that need to be overcome, such as the
complexity of data structures and scalability of the methods, on the
path to realistic systems programs.

Path Invariants

Tom Henzinger

Abstract: The success of software verification depends on the ability to find a suitable abstraction of a program automatically. We present a method for automated abstraction refinement which overcomes some limitations of current predicate discovery schemes. In current schemes, the cause of a false alarm is identified as an infeasible error path, and the abstraction is refined in order to remove that path. By contrast, we view the cause of a false alarm --the spurious counterexample-- as a full-fledged program, namely, a fragment of the original program whose control-flow graph may contain loops and represent unbounded computations. There are two advantages to using such path programs as counterexamples for abstraction refinement. First, we can bring the whole machinery of program analysis to bear on path programs, which are typically small compared to the original program. Specifically, we use constraint-based invariant generation to automatically infer invariants of path programs --so-called path invariants. Second, we use path invariants for abstraction refinement in order to remove not one infeasibility at a time, but at once all (possibly infinitely many) infeasible error computations that are represented by a path program. Unlike previous predicate discovery schemes, our method handles loops without unrolling them; it infers abstractions that involve universal quantification and naturally incorporates disjunctive reasoning.

Joint work with Dirk Beyer, Rupak Majumdar, and Andrey Rybalchenko.

HAVOC: Heap Aware Verification Of C programs￼

Shuvendu Lahiri

Abstract: HAVOC is a tool for
specifying and checking properties of systems software written in C,
similar in spirit to the Spec# effort for C#. The tool understands
low-level pointer manipulations, internal pointers, and cast operations
that are prevalent in systems software. The annotation language of
HAVOC allows the expression of richer properties about the program heap
and data structures such as linked lists and arrays. HAVOC is a modular
verifier. The user provides annotates the program with specifications
and HAVOC checks the annotated program modularly, one procedure at a
time, using an automated theorem prover.

In this talk, I will describe a novel reachability predicate required to reason about linked data structures in the presence of internal pointers and pointer arithmetic. The reachability predicate is at the heart of the annotation language used for describing rich properties of C programs. I will describe our experience with annotating C programs and checking verification conditions using first-order theorem provers, for a set of illustrative C programs in HAVOC.

This is a joint work with Shaz Qadeer.

In this talk, I will describe a novel reachability predicate required to reason about linked data structures in the presence of internal pointers and pointer arithmetic. The reachability predicate is at the heart of the annotation language used for describing rich properties of C programs. I will describe our experience with annotating C programs and checking verification conditions using first-order theorem provers, for a set of illustrative C programs in HAVOC.

This is a joint work with Shaz Qadeer.

Ken McMillan

Abstract:
tba

Amir Pnueli

Abstract: Since most software systems, in particular
those which manipulate heaps, are infinite-state systems, a key technique in
software model checking is based on abstraction which often transforms an
infinite-state system into a finite-state one. A major element in the
application of abstraction is the computation of the abstract transition
relation.

A natural approach to such calculation lifts an abstraction mapping over states into an abstraction of the concrete transition relation. Thus, if "a" is a state abstraction mapping and R is the concrete transition relation then the abstract states S_1 and S_2 are R_a related iff there exist two concrete states s_1 and s_2, such that s_2 is R-related to s_1, a(s_1)=S_1 and a(s_2)=S_2. This defines R_a as the abstract transition relation. A naive application of this method for the calculation of R_a involves an exponential number of invocations of a decision procedure (usually part of a theorem prover such as PVS), one for each pair of abstract states S_1 and S_2.

In our talk we restrict our attention to cases in which the abstract transition relation R_a can be computed according to the above "precise" definition but in a more effective way, using BDD representation rather than explicit enumeration. We characterize the family of heaps (and induced programs) for which this technique is applicable. So far, the classes of data structures which yielded to this method are linked lists with a single descendant or, alternately, nodes having a single parent. We illustrate the technique for the verification of various list reversals, list traversals, and tree traversal algorithms.

The basic abstraction-based techniques are usually applied for the verification of safety properties. We will also present an extension of these methods to "ranking abstraction" which can be used for the verification of liveness properties and arbitrary temporal properties.

This presentation is based on joint work with Ittai Balaban and Lenore Zuck.

A natural approach to such calculation lifts an abstraction mapping over states into an abstraction of the concrete transition relation. Thus, if "a" is a state abstraction mapping and R is the concrete transition relation then the abstract states S_1 and S_2 are R_a related iff there exist two concrete states s_1 and s_2, such that s_2 is R-related to s_1, a(s_1)=S_1 and a(s_2)=S_2. This defines R_a as the abstract transition relation. A naive application of this method for the calculation of R_a involves an exponential number of invocations of a decision procedure (usually part of a theorem prover such as PVS), one for each pair of abstract states S_1 and S_2.

In our talk we restrict our attention to cases in which the abstract transition relation R_a can be computed according to the above "precise" definition but in a more effective way, using BDD representation rather than explicit enumeration. We characterize the family of heaps (and induced programs) for which this technique is applicable. So far, the classes of data structures which yielded to this method are linked lists with a single descendant or, alternately, nodes having a single parent. We illustrate the technique for the verification of various list reversals, list traversals, and tree traversal algorithms.

The basic abstraction-based techniques are usually applied for the verification of safety properties. We will also present an extension of these methods to "ranking abstraction" which can be used for the verification of liveness properties and arbitrary temporal properties.

This presentation is based on joint work with Ittai Balaban and Lenore Zuck.

Symbolic Shape Analysis

Andreas Podelski

(joint work with Thomas Wies)

Abstract: Symbolic Shape
Analysis uses logical formulas to represent sets of graph-like
states. As in three-valued shape analysis, an abstract domain is specified
by node predicates. Symbolic Shape Analysis improves upon
existing shape analyses in terms of degree of automation. It
uses a decision procedure over graphs (such as Mona) in order to
automatically construct the best abstract transformer and to automatically
refine the abstraction based on a spurious counterexample.

Abstraction in Graph Transformation

Arend Rensink

Abstract: Graph transformation
is a theoretically well-founded formalism that is quite suitable for
capturing the dynamic evolution of discrete systems. By interpreting
heap structures as graphs, a certain amount of abstraction is achieved
automatically. However, for a feasible analysis method based on this
formalism it is necessary to abstract further, by collapsing graphs as
is done in shape analysis, and lifting their transformation to the
abstract level. We discuss several types of such graph abstractions, as
well as a general framework for automatically deriving transformations
of the abstract graphs.

Radu Rugina

Abstract:
We present an approach to shape analysis that uses local
reasoning about individual heap cells instead of global
reasoning about entire the entire heap. The key feature is a
local abstraction that describes the state of one single
cell -- the "tracked cell". The analysis uses this
abstraction to reason locally about one cell at a time,
tracking its state through the program. This strategy is
powerful enough to accurately reason about programs that
manipulate recursive structures. At the same time, it makes
it easier to develop efficient and practical
inter-procedural shape analysis algorithms.
We will also discuss the application of shape analysis
with tracked cells to scalable error detection and
compile-time memory management optimizations. In the context
of these applications, the analysis has successfully scaled
to programs of tens of thousands of lines of C and Java
code.

Mooly Sagiv

Abstract:
One of the prevalent questions in shape analysis is how to abstract correlations between different parts of the heap while maintaining the ability to prove interesting properties via abstract interpretation.
This problem was recognized as non-trivial since the early days of shape analysis. Tracking too many correlations leads to state-space explosion and losing important correlations leads to useless analysis. Moreover, even when the important correlations are known, designing abstract transformers is a difficult task as a naïve solution may be expensive and/or imprecise. The problem becomes acute even on tiny programs when concurrency is introduced.
I will present general methods for handling correlations and describe methods for computing sound transformers which track these correlations with applications to sequential and concurrent programs manipulating heap allocated data.

This research is conducted by Roman Manevich in collaboration with B. Cook, J. Berdine, and G. Ramalingam.

This research is conducted by Roman Manevich in collaboration with B. Cook, J. Berdine, and G. Ramalingam.