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.
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.
Constructing quantified invariants using interpolants
Ken McMillan
Abstract:
tba
Shape Analysis with Precise Abstraction
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.
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.
Shape analysis with tracked cells
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.
Partially Disjunctive Shape Analysis
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.