Static Analysis

Frontmatter

Time of Time

Abstract

In his landmark 1977 paper “The Temporal Logic of Programs”, Amir Pnueli gave a fundamental recognition that the ideally nonterminating behavior of ongoing concurrent programs, such as operating systems and protocols, was a vital aspect of program reasoning. As classical approaches to program correctness were based on initial-state/final-state semantics for terminating programs, these approaches were inapplicable to programs where infinite behavior was the norm. To address this shortcoming, Pnueli suggested the use of temporal logic, a formalism for reasoning about change over time originally studied by philosophers, to meaningfully describe and reason about the infinite behavior of programs. This suggestion turned out to be remarkably fruitful. It struck a resonant chord within the formal verification community, and it has had an enormous impact on the development of the area. It matured into an extremely effective mathematical tool for specifying and verifying a vast class of synchronization and coordination problems common in concurrency. Pnueli thus caused a sea-change in the field of program verification, founding the time of reasoning about time, which has been the most successful period in formal methods yet.

E. Allen Emerson

Static Verification for Code Contracts

Abstract

The Code Contracts project [3] at Microsoft Research enables programmers on the .NET platform to author specifications in existing languages such as C# and VisualBasic. To take advantage of these specifications, we provide tools for documentation generation, runtime contract checking, and static contract verification.

This talk details the overall approach of the static contract checker and examines where and how we trade-off soundness in order to obtain a practical tool that works on a full-fledged object-oriented intermediate language such as the .NET Common Intermediate Language.

Manuel Fähndrich

Translation Validation of Loop Optimizations and Software Pipelining in the TVOC Framework

In Memory of Amir Pnueli

Abstract

Translation validation (TV) is the process of proving that the execution of a translator has generated an output that is a correct translation of the input. When applied to optimizing compilers, TV is used to prove that the generated target code is a correct translation of the source program being compiled. This is in contrast to verifying a compiler, i.e. ensuring that the compiler will generate correct target code for every possible source program – which is generally a far more difficult endeavor.

This paper reviews the TVOC framework developed by Amir Pnueli and his colleagues for translation validation for optimizing compilers, where the program being compiled undergoes substantional transformation for the purposes of optimization. The paper concludes with a discussion of how recent work on the TV of software pipelining by Tristan & Leroy can be incorporated into the TVOC framework.

Benjamin Goldberg

Size-Change Termination and Transition Invariants

Abstract

Two directions of recent work on program termination use the concepts of size-change termination resp. transition invariants. The difference in the setting has as consequence the inherent incomparability of the analysis and verification methods that result from this work. Yet, in order to facilitate the crossover of ideas and techniques in further developments, it seems interesting to identify which aspects in the respective formal foundation are related. This paper presents initial results in this direction.

Matthias Heizmann, Neil D. Jones, Andreas Podelski

Using Static Analysis in Space: Why Doing so?

Abstract

This paper presents the point of view of an industrial company of the space domain on static analysis. It first discusses the compatibility of static analysis with the standards applicable for the development of critical embedded software in the European space domain. It then shows the practical impact of such a technology on the software development process. After the presentation of some examples of industrial use of static analysis, it concludes by envisaging the future needs of industry concerning static analysis.

David Lesens

Statically Inferring Complex Heap, Array, and Numeric Invariants

Abstract

We describe Deskcheck, a parametric static analyzer that is able to establish properties of programs that manipulate dynamically allocated memory, arrays, and integers. Deskcheck can verify quantified invariants over mixed abstract domains, e.g., heap and numeric domains. These domains need only minor extensions to work with our domain combination framework.

The technique used for managing the communication between domains is reminiscent of the Nelson-Oppen technique for combining decision procedures, in that the two domains share a common predicate language to exchange shared facts. However, whereas the Nelson-Oppen technique is limited to a common predicate language of shared equalities, the technique described in this paper uses a common predicate language in which shared facts can be quantified predicates expressed in first-order logic with transitive closure.

We explain how we used Deskcheck to establish memory safety of the thttpd web server’s cache data structure, which uses linked lists, a hash table, and reference counting in a single composite data structure. Our work addresses some of the most complex data-structure invariants considered in the shape-analysis literature.

Bill McCloskey, Thomas Reps, Mooly Sagiv

From Object Fields to Local Variables: A Practical Approach to Field-Sensitive Analysis

Abstract

Static analysis which takes into account the value of data stored in the heap is typically considered complex and computationally intractable in practice. Thus, most static analyzers do not keep track of object fields (or fields for short), i.e., they are field-insensitive. In this paper, we propose locality conditions for soundly converting fields into local variables. This way, field-insensitive analysis over the transformed program can infer information on the original fields. Our notion of locality is context-sensitive and can be applied both to numeric and reference fields. We propose then a polyvariant transformation which actually converts object fields meeting the locality condition into variables and which is able to generate multiple versions of code when this leads to increasing the amount of fields which satisfy the locality conditions. We have implemented our analysis within a termination analyzer for Java bytecode.

Elvira Albert, Puri Arenas, Samir Genaim, German Puebla, Diana Vanessa Ramírez Deantes

Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs

Abstract

Proving the termination of a flowchart program can be done by exhibiting a ranking function, i.e., a function from the program states to a well-founded set, which strictly decreases at each program step. A standard method to automatically generate such a function is to compute invariants for each program point and to search for a ranking in a restricted class of functions that can be handled with linear programming techniques. Previous algorithms based on affine rankings either are applicable only to simple loops (i.e., single-node flowcharts) and rely on enumeration, or are not complete in the sense that they are not guaranteed to find a ranking in the class of functions they consider, if one exists. Our first contribution is to propose an efficient algorithm to compute ranking functions: It can handle flowcharts of arbitrary structure, the class of candidate rankings it explores is larger, and our method, although greedy, is provably complete. Our second contribution is to show how to use the ranking functions we generate to get upper bounds for the computational complexity (number of transitions) of the source program. This estimate is a polynomial, which means that we can handle programs with more than linear complexity. We applied the method on a collection of test cases from the literature. We also show the links and differences with previous techniques based on the insertion of counters.

Christophe Alias, Alain Darte, Paul Feautrier, Laure Gonnord

Deriving Numerical Abstract Domains via Principal Component Analysis

Abstract

We propose a new technique for developing ad-hoc numerical abstract domains by means of statistical analysis. We apply Principal Component Analysis to partial execution traces of programs, to find out a “best basis” in the vector space of program variables. This basis may be used to specialize numerical abstract domains, in order to enhance the precision of the analysis. As an example, we apply our technique to interval analysis of simple imperative programs.

Gianluca Amato, Maurizio Parton, Francesca Scozzari

Concurrent Separation Logic for Pipelined Parallelization

Abstract

Recent innovations in automatic parallelizing compilers are showing impressive speedups on multicore processors using shared memory with asynchronous channels. We have formulated an operational semantics and proved sound a concurrent separation logic to reason about multithreaded programs that communicate asynchronously through channels and share memory. Our logic supports shared channel endpoints (multiple producers and consumers) and introduces histories to overcome limitations with local reasoning. We demonstrate how to transform a sequential proof into a parallelized proof that targets the output of the parallelizing optimization DSWP (Decoupled Software Pipelining).

Christian J. Bell, Andrew W. Appel, David Walker

Automatic Abstraction for Intervals Using Boolean Formulae

Abstract

Traditionally, transfer functions have been manually designed for each operation in a program. Recently, however, there has been growing interest in computing transfer functions, motivated by the desire to reason about sequences of operations that constitute basic blocks. This paper focuses on deriving transfer functions for intervals — possibly the most widely used numeric domain — and shows how they can be computed from Boolean formulae which are derived through bit-blasting. This approach is entirely automatic, avoids complicated elimination algorithms, and provides a systematic way of handling wrap-arounds (integer overflows and underflows) which arise in machine arithmetic.

Jörg Brauer, Andy King

Interval Slopes as a Numerical Abstract Domain for Floating-Point Variables

Abstract

The design of embedded control systems is mainly done with model-based tools such as Matlab/Simulink. Numerical simulation is the central technique of development and verification of such tools. Floating-point arithmetic, which is well-known to only provide approximated results, is omnipresent in this activity. In order to validate the behaviors of numerical simulations using abstract interpretation-based static analysis, we present, theoretically and with experiments, a new partially relational abstract domain dedicated to floating-point variables. It comes from interval expansion of non-linear functions using slopes and it is able to mimic all the behaviors of the floating-point arithmetic. Hence it is adapted to prove the absence of run-time errors or to analyze the numerical precision of embedded control systems.

Alexandre Chapoutot

A Shape Analysis for Non-linear Data Structures

Abstract

We present a terminating shape analysis based on Separation Logic for programs that manipulate non-linear data structures such as trees and graphs. The analysis automatically calculates concise invariants for loops, with a level of precision depending on the manipulations applied on each program variable. We report experimental results obtained from running a prototype that implements our analysis on a variety of examples.

Renato Cherini, Lucas Rearte, Javier Blanco

Modelling Metamorphism by Abstract Interpretation

Abstract

Metamorphic malware apply semantics-preserving transformations to their own code in order to foil detection systems based on signature matching. In this paper we consider the problem of automatically extract metamorphic signatures from these malware. We introduce a semantics for self-modifying code, later called phase semantics, and prove its correctness by showing that it is an abstract interpretation of the standard trace semantics. Phase semantics precisely models the metamorphic code behavior by providing a set of traces of programs which correspond to the possible evolutions of the metamorphic code during execution. We show that metamorphic signatures can be automatically extracted by abstract interpretation of the phase semantics, and that regular metamorphism can be modelled as finite state automata abstraction of the phase semantics.

Mila Dalla Preda, Roberto Giacobazzi, Saumya Debray, Kevin Coogan, Gregg M. Townsend

Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis

Abstract

Static analysis techniques that represent program states as formulas typically generate a large number of redundant formulas that are incrementally constructed from previous formulas. In addition to querying satisfiability and validity, analyses perform other operations on formulas, such as quantifier elimination, substitution, and instantiation, most of which are highly sensitive to formula size. Thus, the scalability of many static analysis techniques requires controlling the size of the generated formulas throughout the analysis. In this paper, we present a practical algorithm for reducing SMT formulas to a simplified form containing no redundant subparts. We present experimental evidence that on-line simplification of formulas dramatically improves scalability.

Isil Dillig, Thomas Dillig, Alex Aiken

Compositional Bitvector Analysis for Concurrent Programs with Nested Locks

Abstract

We propose a new technique to perform bitvector data flow analysis for concurrent programs. Our algorithm works for concurrent programs with nested locking synchronization. We show that this algorithm computes precise solutions (meet over all paths) to bitvector problems. Moreover, this algorithm is compositional: it first solves a local (sequential) data flow problem, and then efficiently combines these solutions leveraging reachability results on nested locks [6,7]. We have implemented our algorithm on top of an existing sequential data flow analysis tool, and demonstrate that the technique performs and scales well.

Azadeh Farzan, Zachary Kincaid

Computing Relaxed Abstract Semantics w.r.t. Quadratic Zones Precisely

Abstract

In the present paper we compute numerical invariants of programs by abstract interpretation. For that we consider the abstract domain of quadratic zones recently introduced by Adjé et al. [2]. We use a relaxed abstract semantics which is at least as precise as the relaxed abstract semantics of Adjé et al. [2]. For computing our relaxed abstract semantics, we present a practical strategy improvement algorithm for precisely computing least solutions of fixpoint equation systems, whose right-hand sides use order-concave operators and the maximum operator. These fixpoint equation systems strictly generalize the fixpoint equation systems considered by Gawlitza and Seidl [11].

Thomas Martin Gawlitza, Helmut Seidl

Boxes: A Symbolic Abstract Domain of Boxes

Abstract

Numeric abstract domains are widely used in program analyses. The simplest numeric domains over-approximate disjunction by an imprecise join, typically yielding path-insensitive analyses. This problem is addressed by domain refinements, such as finite powersets, which provide exact disjunction. However, developing correct and efficient disjunctive refinement is challenging. First, there must be an efficient way to represent and manipulate abstract values. The simple approach of using “sets of base abstract values” is often not scalable. Second, while a widening must strike the right balance between precision and the rate of convergence, it is notoriously hard to get correct. In this paper, we present an implementation of the Boxes abstract domain – a refinement of the well-known Box (or Intervals) domain with finite disjunctions. An element of Boxes is a finite union of boxes, i.e., expressible as a propositional formula over upper- and lower-bounds constraints. Our implementation is symbolic, and weds the strengths of Binary Decision Diagrams (BDDs) and Box. The complexity of the operations (meet, join, transfer functions, and widening) is polynomial in the size of the operands. Empirical evaluation indicates that the performance of Boxes is superior to other existing refinements of Box with comparable expressiveness.

Arie Gurfinkel, Sagar Chaki

Alternation for Termination

Abstract

Proving termination of sequential programs is an important problem, both for establishing the total correctness of systems and as a component of proving more general termination and liveness properties. We present a new algorithm, TRex, that determines if a sequential program terminates on all inputs. The key characteristic of TRex is that it alternates between refining an over-approximation and an under-approximation of each loop in a sequential program. In order to prove termination, TRex maintains an over-approximation of the set of states that can be reached at the head of the loop. In order to prove non-termination, it maintains an under-approximation of the set of paths through the body of the loop. The over-approximation and under-approximation are used to refine each other iteratively, and help TRex to arrive quickly at a proof of either termination or non-termination.

TRex refines the approximations in alternation by composing three different program analyses: (1) local termination provers that can quickly handle intricate loops, but not whole programs, (2) non-termination provers that analyze one cycle through a loop, but not all paths, and (3) global safety provers that can check safety properties of large programs, but cannot check liveness properties. This structure allows TRex to be instantiated using any of the pre-existing techniques for proving termination or non-termination of individual loops.

We evaluated TRex by applying it to prove termination or find bugs for a set of real-world programs and termination analysis benchmarks. Our results demonstrate that alternation allows TRex to prove termination or produce certified termination bugs more effectively than previous techniques.

William R. Harris, Akash Lal, Aditya V. Nori, Sriram K. Rajamani

Interprocedural Analysis with Lazy Propagation

Abstract

We propose lazy propagation as a technique for flow- and context-sensitive interprocedural analysis of programs with objects and first-class functions where transfer functions may not be distributive. The technique is described formally as a systematic modification of a variant of the monotone framework and its theoretical properties are shown. It is implemented in a type analysis tool for JavaScript where it results in a significant improvement in performance.

Simon Holm Jensen, Anders Møller, Peter Thiemann

Verifying a Local Generic Solver in Coq

Abstract

Fixpoint engines are the core components of program analysis tools and compilers. If these tools are to be trusted, special attention should be paid also to the correctness of such solvers. In this paper we consider the local generic fixpoint solver RLD which can be applied to constraint systems \({\bf x}\sqsupseteq f_{\bf x},{\bf x}\in V\), over some lattice \(\mathbb{D}\) where the right-hand sides f _x are given as arbitrary functions implemented in some specification language. The verification of this algorithm is challenging, because it uses higher-order functions and relies on side effects to track variable dependences as they are encountered dynamically during fixpoint iterations. Here, we present a correctness proof of this algorithm which has been formalized by means of the interactive proof assistant Coq.

Martin Hofmann, Aleksandr Karbyshev, Helmut Seidl

Thread-Modular Counterexample-Guided Abstraction Refinement

Abstract

We consider the refinement of a static analysis method called thread-modular verification. It was an open question whether such a refinement can be done automatically. We present a counterexample-guided abstraction refinement algorithm for thread-modular verification and demonstrate its potential, both theoretically and practically.

Alexander Malkis, Andreas Podelski, Andrey Rybalchenko

Generating Invariants for Non-linear Hybrid Systems by Linear Algebraic Methods

Abstract

We describe powerful computational methods, relying on linear algebraic methods, for generating ideals for non-linear invariants of algebraic hybrid systems. We show that the preconditions for discrete transitions and the Lie-derivatives for continuous evolution can be viewed as morphisms and so can be suitably represented by matrices. We reduce the non-trivial invariant generation problem to the computation of the associated eigenspaces by encoding the new consecution requirements as specific morphisms represented by matrices. More specifically, we establish very general sufficient conditions that show the existence and allow the computation of invariant ideals. Our methods also embody a strategy to estimate degree bounds, leading to the discovery of rich classes of inductive, i.e. provable, invariants. Our approach avoids first-order quantifier elimination, Grobner basis computation or direct system resolution, thereby circumventing difficulties met by other recent techniques.

Nadir Matringe, Arnaldo Vieira Moura, Rachid Rebiha

Linear-Invariant Generation for Probabilistic Programs:

Automated Support for Proof-Based Methods

Abstract

We present a constraint-based method for automatically generating quantitative invariants for linear probabilistic programs, and we show how it can be used, in combination with proof-based methods, to verify properties of probabilistic programs that cannot be analysed using existing automated methods. To our knowledge, this is the first automated method proposed for quantitative-invariant generation.

Joost-Pieter Katoen, Annabelle K. McIver, Larissa A. Meinicke, Carroll C. Morgan

Abstract Interpreters for Free

Abstract

In small-step abstract interpretations, the concrete and abstract semantics bear an uncanny resemblance. In this work, we present an analysis-design methodology that both explains and exploits that resemblance. Specifically, we present a two-step method to convert a small-step concrete semantics into a family of sound, computable abstract interpretations. The first step re-factors the concrete state-space to eliminate recursive structure; this refactoring of the state-space simultaneously determines a store-passing-style transformation on the underlying concrete semantics. The second step uses inference rules to generate an abstract state-space and a Galois connection simultaneously. The Galois connection allows the calculation of the “optimal” abstract interpretation. The two-step process is unambiguous, but nondeterministic: at each step, analysis designers face choices. Some of these choices ultimately influence properties such as flow-, field- and context-sensitivity. Thus, under the method, we can give the emergence of these properties a graph-theoretic characterization. To illustrate the method, we systematically abstract the continuation-passing style lambda calculus to arrive at two distinct families of analyses. The first is the well-known k-CFA family of analyses. The second consists of novel “environment-centric” abstract interpretations, none of which appear in the literature on static analysis of higher-order programs.

Matthew Might

Points-to Analysis as a System of Linear Equations

Abstract

We propose a novel formulation of the points-to analysis as a system of linear equations. With this, the efficiency of the points-to analysis can be significantly improved by leveraging the advances in solution procedures for solving the systems of linear equations. However, such a formulation is non-trivial and becomes challenging due to various facts, namely, multiple pointer indirections, address-of operators and multiple assignments to the same variable. Further, the problem is exacerbated by the need to keep the transformed equations linear. Despite this, we successfully model all the pointer operations. We propose a novel inclusion-based context-sensitive points-to analysis algorithm based on prime factorization, which can model all the pointer operations. Experimental evaluation on SPEC 2000 benchmarks and two large open source programs reveals that our approach is competitive to the state-of-the-art algorithms. With an average memory requirement of mere 21MB, our context-sensitive points-to analysis algorithm analyzes each benchmark in 55 seconds on an average.

Rupesh Nasre, Ramaswamy Govindarajan

Strictness Meets Data Flow

Abstract

Properties of programs can be formulated using various techniques: dataflow analysis, abstract interpretation and type-like inference systems. This paper reconstructs strictness analysis (establishing when function parameters are evaluated in a lazy language) as a dataflow analysis by expressing the dataflow properties as an effect system. Strictness properties so expressed give a clearer operational understanding and enable a range of additional optimisations including implicational strictness. At first order strictness effects have the expected principality properties (best-property inference) and can be computed simply.

Tom Schrijvers, Alan Mycroft

Automatic Verification of Determinism for Structured Parallel Programs

Abstract

We present a static analysis for automatically verifying determinism of structured parallel programs. The main idea is to leverage the structure of the program to reduce determinism verification to an independence property that can be proved using a simple sequential analysis. Given a task-parallel program, we identify program fragments that may execute in parallel and check that these fragments perform independent memory accesses using a sequential analysis. Since the parts that can execute in parallel are typically only a small fraction of the program, we can employ powerful numerical abstractions to establish that tasks executing in parallel only perform independent memory accesses. We have implemented our analysis in a tool called Dice and successfully applied it to verify determinism on a suite of benchmarks derived from those used in the high-performance computing community.

Martin Vechev, Eran Yahav, Raghavan Raman, Vivek Sarkar

Backmatter