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.

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.

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.
 

Abstract: tba

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.

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.

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.

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.

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.