# SAS 2013: Accepted Papers with Abstracts

Leo White and Alan Mycroft. Concise analysis using implication algebras for task-local memory optimisation
Abstract: OpenMP is a pragma-based extension to C to support parallelism. The OpenMP standard recently added support for task-based parallelism but in a richer way than languages such as Cilk. Naive implementations give each task its own stack for task-local memory, which is very inefficient.
We detail a program analysis for OpenMP to enable tasks to share stacks without synchronisation -- either unconditionally or dependent on some cheap run-time condition which is very likely to hold in busy systems. The analysis is based on a novel implication-algebra generalisation of logic programming which allows concise but easily readable encodings of the various constraints. The formalism enables an easy proof of the analysis having a unique solution and being polynomial-time.We conclude with performance figures.
Sandrine Blazy, Vincent Laporte, André Maroneze and David Pichardie. Formal Verification of a C Value Analysis Based on Abstract Interpretation
Abstract: Static analyzers based on abstract interpretation are complex pieces of software implementing delicate algorithms. Even if static analysis techniques are well understood, their implementation on real languages is still error prone.

This paper presents a formal verification using the Coq proof assistant: a formalization of a value analysis (based on abstract interpretation), and a soundness proof of the value analysis. The formalization relies on generic interfaces. The mechanized proof is facilitated by a translation validation of a Bourdoncle fixpoint iterator.

The work has been integrated into the CompCert verified C compiler. Our verified analysis directly operates over an intermediate language of the compiler having the same expressiveness as C. The automatic extraction of our value analysis into OCaml yields a program with competitive results, obtained from experiments on a number of benchmarks and comparisons with the Frama-C tool.
Graeme Gange, Jorge A Navas, Peter Schachte, Harald Sondergaard and Peter Stuckey. Abstract Interpretation over Non-Lattice Abstract Domains
Abstract: The classical theoretical framework for static analysis of programs is abstract interpretation. Much of the power and elegance of that framework rests on the assumption that an abstract domain is a lattice. Nonetheless, and for good reason, the literature on program analysis provides many examples of non-lattice domains, including non-convex numeric domains. The lack of domain structure, however, has negative consequences, both for the precision of program analysis and for the termination of standard Kleene iteration. In this paper we explore these consequences and present general remedies.
Alexis Fouilhe, David Monniaux and Michaël Périn. Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra
Abstract: Polyhedra form an established abstract domain for
infering runtime properties of programs using abstract interpretation.
Computations on them need to be certified for the whole static analysis results to be trusted.
In this work, we look at how far we can get down the road of a posteriori verification
to lower the overhead of certification of the abstract domain of polyhedra.
We demonstrate methods for making the cost of inclusion certificate generation negligible.
Our single-representation, constraints-based implementation compares
with state-of-the-art implementations, performance-wise.
Subhajit Roy. From Concrete Examples to Heap Manipulating Programs
Abstract: Data-structure manipulation is not only a perplexing ordeal for newbies but also a tedious errand for seasoned programmers. Even after a programmer gets the "hang of things", programming complex pointer manipulations (like reversing a link-list) still makes one reach for a notebook to draw "box-and-arrow" diagrams to work out the low-level pointer jugglery. These diagrams are, not surprisingly, used as a basic tool to introduce heap manipulations in introductory programming courses.

We propose a synthesis technology to automatically create programs that manipulate heap data-structures from such diagrams. The programmer is needed to provide a set of concrete examples of her high-level strategy for the low-level manipulations to be discharged automatically. We plan the synthesis task as a sequence of "fast" stages, making it usable in an integrated development environment. We envisage that such a tool will be useful to programmers as a code-assist comfortably tucked away in their favourite integrated development environment.
Kamil Dudka, Petr Peringer and Tomas Vojnar. Byte-Precise Verification of Low-Level List Manipulation
Abstract: We propose a new approach to formal verification of programs that use a low-level list manipulation. Such manipulation includes pointer arithmetic, safe usage of pointers with invalid targets, block operations with memory, reinterpretation of the memory contents, address alignment, etc. Our approach is based on a new representation of sets of heaps which is to some degree inspired by works on separation logic with higher order list predicates, but it is graph-based and uses a more fine-grained (byte-precise) memory model in order to be able to deal with the various low-level memory operations. The approach has been implemented in the Predator tool and successfully validated on multiple non-trivial case studies problematic for state-of-the-art fully automatic shape analysis tools.
The Abstract Domain of Segmented Ranking Functions
Abstract: We present a parameterized abstract domain for proving program termination by abstract interpretation. The domain automatically synthesizes piecewise-defined ranking functions and infers sufficient conditions for program termination. The analysis uses over-approximations but we prove its soundness, meaning that all program executions respecting these sufficient conditions are indeed terminating.

The abstract domain is parameterized by a numerical abstract domain for environments and a numerical abstract domain for functions. This parameterization allows to easily tune the trade-off between precision and cost of the analysis. We describe an instantiation of this generic domain with intervals and affine functions. We define all abstract operators, including widening to ensure convergence.

The analysis does not rely on assumptions about the structure of the analyzed program: for example, it is not limited to simple loops.

To illustrate the potential of the proposed framework, we have implemented a research prototype static analyzer, for a small imperative language, that yielded interesting preliminary results.
Localizing widening and narrowing
Abstract: We show two strategies which may be easily applied to standard abstract interpretation-based static analyzers. They consist in 1) restricting the scope of widening, and 2) intertwining the computation of ascending and descending chains. Using these optimizations it is possible to improve the precision of the analysis,
without any change to the abstract domains.
Precise slicing in imperative programs via term-rewriting and abstract interpretation
Abstract: We propose a new approach for producing precise constrained slices of
programs in a language such as C. We build upon a previous precise approach
for this setting, which is based on term-rewriting, which includes a rich
notion of path-sensitivity, but is primarily targeted at loop-free
fragments. We incorporate abstract interpretation into term-rewriting,
using a given arbitrary abstract domain. Our approach is novel in the
setting of analysis of imperative programs; it is able to slice looping
programs, with precision that is linked to the power of the given abstract
lattice, and a guarantee of termination when the abstract lattice is of
finite height. We address pointers in a first-class manner, including when
they are used within loops to traverse and update recursive data
structures. We illustrate the comparative precision of our slices over
those of previous approaches using two challenging examples, namely, a
program that uses integer arithmetic within a loop, and a program that
traverses and manipulates linked lists, by plugging in an interval domain
and a shape-analysis domain, respectively, into our analysis.
Local Shape Analysis for Overlaid Data Structures
Abstract: We present a shape analysis for programs that manipulate overlaid data structures, which share the same set of objects. The abstract domain contains Separation Logic formulas that (1) combine a per-object separating conjunction with a per-field separating conjunction and (2) constrain a set of variables interpreted as sets of objects. The definition of the abstract domain operators is based on a notion of homomorphism between formulas, viewed as graphs, used recently to define optimal decision procedures for fragments of Separation Logic. Based on a Frame Rule that supports the two versions of separating conjunction, the analysis is able to reason in a modular manner about non-overlaid data structures and then, compose information only at a few program points, e.g., procedure returns.
Emanuele D'Osualdo, Jonathan Kochems and C.-H. Luke Ong. Automatic Verification of Erlang-Style Concurrency
Abstract: This paper presents an approach to verify safety properties of Erlang-style,
higher-order concurrent programs automatically. Inspired by Core Erlang, we
introduce Lambda-Actor, a prototypical functional language with pattern-matching
algebraic data types, augmented with process creation and asynchronous
message-passing primitives. We formalise an abstract model of Lambda-Actor
programs called Actor Communicating System (ACS) which has a natural
interpretation as a vector addition system, for which some verification problems
are decidable. We give a parametric abstract interpretation framework for
Lambda-Actor and use it to build a polytime computable, flow-based, abstract
semantics of Lambda-Actor programs, which we then use to bootstrap the ACS
construction, thus deriving a more accurate abstract model of the input program.
We have constructed Soter, a tool implementation of the verification method,
thereby obtaining the first fully-automatic, infinite-state model checker for a
core fragment of Erlang. We find that in practice our abstraction technique is
accurate enough to verify an interesting range of safety properties. Though the
ACS coverability problem is Expspace-complete, Soter can analyse interesting
programs in a matter of seconds.
Hila Peleg, Sharon Shoham, Eran Yahav and Hongseok Yang. Symbolic Automata for Static Specification Mining
Abstract: We present a formal framework for static specification mining. The main idea is to represent partial temporal specifications as symbolic automata — automata where transitions may be labelled by variables, and a variable can be substituted by a letter, a word, or a regular language. Using symbolic automata, we construct an abstract domain for static specification mining, capturing both the partialness of a specification and the precision of a specification. We show interesting relationships between lattice operations of this domain and common operators for manipulating partial temporal specifications, such as building a more informative specification by consolidating two partial specifications.
Nimrod Partush and Eran Yahav. Abstract Semantic Differencing for Numerical Programs
Abstract: We address the problem of computing semantic differences between a program and a patched version of the program. Our goal is to obtain a precise characterization of the difference between program versions, or establish their equivalence when no difference exists.

We focus on computing semantic differences in numerical programs where the values of variables have no a-priori bounds, and use abstract interpretation to compute an over-approximation of program differences. Computing differences and establishing equivalence under abstraction requires abstracting relationships between variables in the two programs. Towards that end, we first construct a \emph{correlating program} in which these relationships can be tracked, and then use a correlating abstract domain to compute a sound approximation of these relationships. To better establish equivalence between correlated variables and precisely capture differences, our domain has to represent non-convex information. To balance precision and cost of this representation, our domain may over-approximate numerical information as long as equivalence between correlated variables is preserved.

We have implemented our approach in a tool called DIZY, built on the LLVM compiler infrastructure and the APRON numerical abstract domain library, and applied it to a number of challenging real-world examples, including programs from the GNU core utilities, Mozilla Firefox and the Linux Kernel. Our evaluation shows that DIZY often manages to establish equivalence, describes precise approximation of semantic differences when difference exists, and reports only a few false differences.
Automatic Synthesis of Deterministic Concurrency
Abstract: Many parallel programs are meant to be deterministic: for the same input, the program must produce the same output, regardless of scheduling choices. Unfortunately, due to complex parallel interaction, programmers make subtle mistakes that lead to violations of determinism.

In this paper, we present a framework for static synthesis of deterministic concurrency control: given a non-deterministic parallel program, our synthesis algorithm introduces synchronization that transforms the program into a deterministic one. The main idea is to statically compute inter-thread ordering constraints that both guarantee determinism and preserve program termination. Then, given the constraints and a set of synchronization primitives, the synthesizer produces a program that enforces the constraints using the provided synchronization primitives.

To handle real-world programs, our synthesis algorithm uses two abstractions: a thread-modular abstraction, and an abstraction for memory locations that can track array accesses. We have implemented our algorithm and successfully applied it to synthesize deterministic control for several challenging programs inspired by those used in the high-performance computing community. For most programs the synthesizer produced synchronization that is as good or better than the hand-crafted synchronization inserted by the programmer.
Martin Brain, Vijay D'Silva, Alberto Griggio, Leopold Haller and Daniel Kroening. Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL
Abstract: Several modern program verification algorithms are built upon interpolating decision procedures. Abstract Conflict Driven Clause Learning (ACDCL) lifts the Conflict Driven Clause Learning algorithm in SAT solvers to abstract domains, and leads to a family of decision procedures for a variety of theories. In this paper, we present an interpolation algorithm for ACDCL procedures. We identify a family of abstract domains for which interpolation reduces to the propositional interpolation algorithm, and requires only linear time in the size of a proof. We instantiate our procedure to derive the first interpolation procedure for floating-point logic, and subsequently, the first interpolation-based verifiers for programs with floating-point variables. We empirically demonstrate the potential of the approach by verifying a number of programs which are challenging for current verification tools.
Hyunha Kim, Kyung-Goo Doh and David Schmidt. Static validation of dynamically generated HTML documents based on abstract parsing and semantic processing
Abstract: Abstract parsing is a static-analysis technique for a program that, given a reference LR(k) context-free grammar, statically checks whether or not every dynamically generated string output by the program conforms to the grammar. The technique operates by applying an LR(k) parser for the reference language to data-flow equations extracted from the program, immediately parsing all the possible string outputs to validate their syntactic well-formedness.

In this paper, we extend abstract parsing to do semantic-attribute processing and apply this extension to statically verify that HTML documents generated by JSP or PHP are always valid according to the HTML DTD. This application is necessary because the HTML DTD cannot be fully described as an LR(k) grammar. We completely define the HTML 4.01 Transitional DTD in an attributed LALR(1) grammar, carry out experiments for selected real-world JSP and PHP applications, and expose numerous HTML validation errors in the applications. In the process, we experimentally show that semantic properties defined by attribute grammars can also be verified using our technique.
Predicate Abstraction for Relaxed Memory Models
Abstract: We present a novel approach for predicate abstraction of programs running on relaxed memory models. Our approach consists of two steps.

First, we reduce the problem of verifying a program $P$ running on a memory model $M$
to the problem of verifying a program $P_M$ that captures an abstraction of $M$ as part of the program.

Second, we show how to discover new predicates that enable verification of $P_M$.
The core idea is to extrapolate from the predicates used to verify $P$ under sequential consistency. A key new concept is that of cube extrapolation: it successfully avoids exponential explosion when abstracting $P_M$.

We implemented our approach for the x86 TSO and PSO memory models and showed that predicates discovered via extrapolation are powerful enough to verify several challenging concurrent programs. We show that our cube extrapolation approach introduces a x100 reduction in the number of SMT calls for several programs, enabling their verification. This is the first time some of these programs have been verified for a model as relaxed as PSO.
Rahul Sharma, Saurabh Gupta, Bharath Hariharan, Alex Aiken and Aditya Nori. Verification as Learning Geometric Concepts
Abstract: We formalize the problem of program verification as a learning problem, showing that invariants in program verification can be regarded as geometric concepts in machine learning. Safety properties define bad states: states a program should not reach. Program verification explains why a program’s set of reachable states is disjoint from the set of bad states. In Hoare Logic, these explanations are predicates that form inductive assertions. Using samples for reachable and bad states and by applying well known machine learning algorithms for classification, we are able to generate inductive assertions. By relaxing the search for an exact proof to classifiers, we obtain complexity theoretic improvements. Further, we extend the learning algorithm to obtain a sound procedure that can generate proofs containing invariants that are arbitrary boolean combinations of polynomial inequalities. We have evaluated our approach on a number of challenging benchmarks and the results are promising.
Witnessing Program Transformations
Abstract:
We study two closely related problems: (a) showing that a program transformation is correct and (b) propagating a program invariant through a sequence of transformations. The second problem is motivated by an application where invariants on a program are used to enhance both the scope and the quality of the optimizations applied during compilation. We show that both problems can be addressed by generating, at compile-time, a witness for every instance of a transformation. A witness may be checked independently to establish the correctness of the transformation and, if correct, a witness helps transfer invariants from the source to the target program. This approach is simpler than proving correctness of the transformation over all inputs, and more comprehensive than translation validation heuristics, which are limited to specific transformations. We prove that stuttering simulation is a complete witness format: every correct transformation has a witness that is a stuttering simulation relation. Moreover, stuttering simulation witnesses compose, resulting in a single witness for a sequence of transformations. We define simulation witnesses for a number of standard compiler optimizations; this exercise indicates that witness generation is usually much simpler than the corresponding optimization procedure.
Pranav Garg, P. Madhusudan and Gennaro Parlato. Quantified Data Automata on Skinny Trees: an Abstract Domain for Lists
Abstract: We propose a new approach to heap analysis through an abstract domain
of automata, called automatic shapes. The abstract domain uses a particular kind of automata, called *quantified data automata on skinny trees* (QSDAs), that allows to define universally quantified properties of singly-linked lists. To ensure convergence of the abstract fixed-point computation, we introduce a sub-class of QSDAs called elastic QSDAs, which also form an abstract domain. We evaluate our approach on several list manipulating programs and we show that the proposed domain is powerful enough to prove a large class of these programs correct.
On Solving Universally Quantified Horn Clauses
Abstract: Program proving can be viewed as solving for uknown relations (such
as loop invariants, procedure summaries and so on) that occur in the
logical verification conditions of a program, such that the
verification conditions are valid. Generic logical tools exist that
can solve such problems modulo certain background theories, and
therefore can be used for program analysis. Here, we extend these
techniques to solve for \emph{quantified} relations. This makes it
possible to guide the solver by constraining the form of the proof,
allowing it to converge when it othwise would not. We show how to
simulate existing abstract domains in this way, without having to directly
implement program analyses or make certain heuristic choices, such as
the terms and predicates that form the parameters of the abstact
domain. Moreover, the approach gives the flexibility to go beyond
these domains and experiment quickly with various invariant forms.
Rupak Majumdar, Roland Meyer and Zilong Wang. Static Provenance Verification for Message Passing Programs
Abstract: Provenance information records the source and ownership history of an object.
We study the problem of provenance tracking in concurrent programs, where several principals exchange messages over unbounded but unordered channels.
The provenance of a message, roughly, is a function of the sequence of principals that have transmitted the message.
The provenance verification problem is to statically decide, given a message passing program and a set of allowed provenances, whether the provenance of all messages in all possible program executions, belongs to the allowed set.
We formalize the provenance verification problem abstractly in terms of well-structured provenance domains, and show a general decidability result for it.
In particular, we show that if the provenance of a message is a sequence of principals who have sent the message, and a provenance query asks if the provenance lies in a regular set, the problem is decidable and EXPSPACE-complete.
While the theoretical complexity is high, we show an implementation of our technique that performs efficiently on a set of Javascript examples tracking provenances in Firefox extensions.
Our experiments show that many browser extensions store and transmit user information although the user sets the browser to the private mode.
Peter Lammich, Alexander Wenner, Markus Müller-Olm and Helmut Seidl. Contextual Locking for Dynamic Pushdown Networks
Abstract: Contextual locking
is a scheme for synchronizing between possibly recursive processes,
which allows for arbitrary usage of locks within the same procedure call.
It has been introduced by Chadha et al. where it is
shown that control-point reachablitiy for two such processes
is decidable in polynomial time.

Here, we complement these results.
We show that in presence of contextual locking,
control-point reachablitiy becomes PSPACE-hard, already if the number
of processes is increased to three.

On the other hand, we show that PSPACE is both necessary and sufficient
for deciding control-point reachablitiy of k processes for k>2, and
that this upper bound still holds
if dynamic spawning of new processes is allowed.

Furthermore, we consider the problem of regular reachability, i.e.,
whether a configuration within a given regular set can be reached.
Here, we show that this problem is decidable for recursive processes with
dynamic thread creation and contextual locking.
Finally, we generalize this result to processes that additionally
use simple forms of join operations.