Documents
A Specialization Calculus for Pruning Disjunctive Predicates to Support Verification
Separation logic-based abstraction mechanisms, enhanced with userdefined inductive predicates, represent a powerful, expressive means of specifying heap-based data structures with strong invariant properties. However, expressive power comes at a cost: the manipulation of such logics typically requires the unfolding of disjunctive predicates which may lead to expensive proof search. We address this problem by proposing a predicate specialization technique that allows efficient symbolic pruning of infeasible disjuncts inside each predicate instance. Our technique is presented as a calculus whose derivations preserve the satisfiability of formulas, while reducing the subsequent cost of their manipulation. Initial experimental results have confirmed significant speed gains from the deployment of predicate specialization. While specialization is a familiar technique for code optimization, its use in program verification is new.
Practical, low-effort equivalence verification of real code
Verifying code equivalence is useful in many situations, such as checking: yesterday’s code against today’s, different implementations of the same (standardized) interface, or an optimized routine against a reference implementation. We present a tool designed to easily check the equivalence of two arbitrary C functions. The tool provides guarantees far beyond those possible with testing, yet it often requires less work than writing even a single test case. It automatically synthesizes inputs to the routines and uses bit-accurate, sound symbolic execution to verify that they produce equivalent outputs on a finite number of paths, even for rich, nested data structures. We show that the approach works well, even on heavily-tested code, where it finds interesting errors and gets high statement coverage, often exhausting all feasible paths for a given input size. We also show how the simple trick of checking equivalence of identical code turns the verification tool chain against itself, finding errors in the underlying compiler and verification tool. 1 Introduction
Simplifying Loop Invariants Generation Using Splitter Predicates
We present a novel static analysis technique that substan- tially improves the quality of invariants inferred by standard loop invari- ant generation techniques. Our technique decomposes multi-phase loops, which require disjunctive invariants, into a semantically equivalent se- quence of single-phase loops, each of which requires simple, conjunctive invariants. We dene splitter predicates which are used to identify phase transitions in loops, and we present an algorithm to nd useful split- ter predicates that enable the phase-reducing transformation. We show experimentally on a set of representative benchmarks from the litera- ture and real code examples that our technique substantially increases the quality of invariants inferred by standard invariant generation tech- niques. Our technique is conceptually simple, easy to implement, and can be integrated into any automatic loop invariant generator.
Temporal property verification as a program analysis task
We describe a reduction from temporal property verification to a program analysis problem. We produce an encoding which, with the use of recursion and nondeterminism, enables off-the-shelf program analysis tools to naturally perform the reasoning necessary for proving temporal properties (e.g. backtracking, eventuality checking, tree counterexamples for branching-time properties, abstraction refinement, etc.). Using examples drawn from the PostgreSQL database server, Apache web server, and Windows OS kernel, we demonstrate the practical viability of our work.
Precondition Inference from Intermittent Assertions and Application to Contracts on Collections
Programmers often insert assertions in their code to be optionally checked at runtime, at least during the debugging phase. In the context of design by contracts, these assertions would better be given as a precondition of the method/procedure which can detect that a caller has violated the procedure's contract in a way which denitely leads to an assertion violation (e.g., for separate static analysis). We dene precisely and formally the contract inference problem from intermittent assertions inserted in the code by the programmer. Our denition excludes no good run even when a non-deterministic choice (e.g., an interactive input) could lead to a bad one (so this is not the weakest precondition, nor its strengthening by abduction, since a terminating successful execution is not guaranteed). We then introduce new ab- stract interpretation-based methods to automatically infer both the static contract precondition of a method/procedure and the code to check it at runtime on scalar and collection variables.
Path Invariants
The success of software verification depends on the ability to find a suitable abstraction of a program automatically. We propose 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.
Interpolation-based Software Verification with WOLVERINE
Wolverine is a software verication tool using Craig interpolation to compute invariants of ANSI-C and C++ programs. The tool is an implementation of the lazy abstraction approach, generating a reachability tree by unwinding the transition relation of the input program and annotating its nodes with interpolants representing safe states. Wolverine features a built-in interpolating decision procedure for equality logic with uninterpreted functions which provides limited support for bit-vector operations. In addition, it provides an API enabling the integration of other interpolating decision procedures, making it a valuable source of benchmarks and allowing it to take advantage of the continuous performance improvements of SMT solvers.We evaluate the performance ofWolverine by comparing it to the predicate abstraction-based verier SatAbs on a number of verication conditions of Linux device drivers.
CPACHECKER: A Tool for Configurable Software Verification
Configurable software verification is a recent concept for expressing different program analysis and model checking approaches in one single formalism. This paper presents CPAchecker, a tool and framework that aims at easy integration of new verification components. Every abstract domain, together with the corresponding operations, is required to implement the interface of configurable program analysis (CPA). The main algorithm is configurable to perform a reachability analysis on arbitrary combinations of existing CPAs. The major design goal during the development was to provide a framework for developers that is flexible and easy to extend. We hope that researchers find it convenient and productive to implement new verification ideas and algorithms using this platform and that it advances the field by making it easier to perform practical experiments. The tool is implemented in Java and runs as command-line tool or as Eclipse plug-in. We evaluate the efficiency of our tool on benchmarks from the software model checker Blast. The first released version of CPAchecker implements CPAs for predicate abstraction, octagon, and explicit-value domains. Binaries and the source code of CPAchecker are publicly available as free software.