Verification, Model Checking, and Abstract Interpretation

Frontmatter

Are Cells Asynchronous Circuits?

(Invited Talk)

Abstract

Cells do not seem to have “clocks” in the same sense as synchronous sequential digital circuits. But cells must operate extremely reliably in spite of large amounts of noise and environmental variations which would result in timing variation in a Boolean model of cellular control.

David L. Dill

Formal Analysis of Message Passing

(Invited Talk)

Abstract

The message passing paradigm underlies many important families of programs—for instance programs in the area of high performance computing that support science and engineering research. Unfortunately, very few formal methods researchers are involved in developing formal analysis tools and techniques for message passing programs. This paper summarizes research being done in our groups in support of this area, specifically with respect to the Message Passing Interface. We emphasize the need for specialized varieties of many familiar notions such as deadlock detection, race analysis, symmetry analysis, partial order reduction, static analysis and symbolic reasoning support. Since these issues are harbingers of those being faced in multicore programming, the time is ripe to build a critical mass of researchers working in this area.

Stephen F. Siegel, Ganesh Gopalakrishnan

Practical Verification for the Working Programmer with CodeContracts and Abstract Interpretation

(Invited Talk)

Abstract

CodeContracts provide a language agnostic way to specify and check preconditions, postconditions and object invariants (collectively called contracts [17]). Specifications take the form of calls to static methods of a Contract library [7]. The authoring library is available out-of-the-box to all .NET programmers from υ4.

Francesco Logozzo

Quality Engineering: Leveraging Heterogeneous Information

(Invited Talk)

Abstract

In this paper we present a flexible framework for fine tuning the quality of program analysis based on variations, generalizations, and pragmatic extensions of Plotkin’s Structured Operational Semantics (SOS). Key to these variations is the idea of Property-Oriented Expansion, here the non-standard use of the data component in SOS configurations, which ranges from simple abstract interpretations, over arbitrary data flow information, to e.g., temporal constraints. In its most general form, which is characterized by the notion of unifying models, this results in a framework not only for fine-tuning program analysis according to an aspect (quality) of choice, but also for synthesizing orchestrations for service-oriented applications based on loose temporal specifications. From an engineering perspective, the simple interface pattern underlying the unifying models approach was key for realizing our experimental platform. Our experimental results, in particular concerning the state explosion problem, indicate that, in practice, limiting the expansion to the previously determined areas of impact suffices to keep the code growth quite moderate.

Bernhard Steffen, Oliver Rüthing

More Precise Yet Widely Applicable Cost Analysis

Abstract

Cost analysis aims at determining the amount of resources required to run a program in terms of its input data sizes. Automatically inferring precise bounds, while at the same time being able to handle a wide class of programs, is a main challenge in cost analysis. (1) Existing methods which rely on computer algebra systems (CAS) to solve the obtained cost recurrence equations (CR) are very precise when applicable, but handle a very restricted class of CR. (2) Specific solvers developed for CR tend to sacrifice accuracy for wider applicability. In this paper, we present a novel approach to inferring precise upper and lower bounds on CR which, when compared to (1), is strictly more widely applicable while precision is kept and when compared to (2), is in practice more precise (obtaining even tighter complexity orders), keeps wide applicability and, besides, can be applied to obtain useful lower bounds as well. The main novelty is that we are able to accurately bound the worst-case/best-case cost of each iteration of the program loops and, then, by summing the resulting sequences, we achieve very precise upper/lower bounds.

Elvira Albert, Samir Genaim, Abu Naser Masud

Refinement-Based CFG Reconstruction from Unstructured Programs

Abstract

This paper addresses the issue of recovering a both safe and precise approximation of the Control Flow Graph (CFG) of an unstructured program, typically an executable file. The problem is tackled in an original way, with a refinement-based static analysis working over finite sets of constant values. Requirement propagation allows the analysis to automatically adjust the domain precision only where it is needed, resulting in precise CFG recovery at moderate cost. First experiments, including an industrial case study, show that the method outperforms standard analyses in terms of precision, efficiency or robustness.

Sébastien Bardin, Philippe Herrmann, Franck Védrine

SAT-Based Model Checking without Unrolling

Abstract

A new form of SAT-based symbolic model checking is described. Instead of unrolling the transition relation, it incrementally generates clauses that are inductive relative to (and augment) stepwise approximate reachability information. In this way, the algorithm gradually refines the property, eventually producing either an inductive strengthening of the property or a counterexample trace. Our experimental studies show that induction is a powerful tool for generalizing the unreachability of given error states: it can refine away many states at once, and it is effective at focusing the proof search on aspects of the transition system relevant to the property. Furthermore, the incremental structure of the algorithm lends itself to a parallel implementation.

Aaron R. Bradley

Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic

Abstract

Craig interpolation has emerged as an effective means of generating candidate program invariants. We present interpolation procedures for the theories of Presburger arithmetic combined with (i) uninterpreted predicates (QPA+UP), (ii) uninterpreted functions (QPA+UF) and (iii) extensional arrays (QPA+AR). We prove that none of these combinations can be effectively interpolated without the use of quantifiers, even if the input formulae are quantifier-free. We go on to identify fragments of QPA+UP and QPA+UF with restricted forms of guarded quantification that are closed under interpolation. Formulae in these fragments can easily be mapped to quantifier-free expressions with integer division. For QPA+AR, we formulate a sound interpolation procedure that potentially produces interpolants with unrestricted quantifiers.

Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl

Probabilistic Büchi Automata with Non-extremal Acceptance Thresholds

Abstract

This paper investigates the power of Probabilistic Büchi Automata (PBA) when the threshold probability of acceptance is non-extremal, i.e., is a value strictly between 0 and 1. Many practical randomized algorithms are designed to work under non-extremal threshold probabilities and thus it is important to study power of PBAs for such cases.

The paper presents a number of surprising expressiveness and decidability results for PBAs when the threshold probability is non-extremal. Some of these results sharply contrast with the results for extremal threshold probabilities. The paper also presents results for Hierarchical PBAs and for an interesting subclass of them called simple PBAs.

Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan

Synthesis of Fault-Tolerant Embedded Systems Using Games: From Theory to Practice

Abstract

In this paper, we present an approach for fault-tolerant synthesis by combining predefined patterns for fault-tolerance with algorithmic game solving. A non-fault-tolerant system, together with the relevant fault hypothesis and fault-tolerant mechanism templates in a pool are translated into a distributed game, and we perform an incomplete search of strategies to cope with undecidability. The result of the game is translated back to executable code concretizing fault-tolerant mechanisms using constraint solving. The overall approach is implemented to a prototype tool chain and is illustrated using examples.

Chih-Hong Cheng, Harald Rueß, Alois Knoll, Christian Buckl

Proving Stabilization of Biological Systems

Abstract

We describe an efficient procedure for proving stabilization of biological systems modeled as qualitative networks or genetic regulatory networks. For scalability, our procedure uses modular proof techniques, where state-space exploration is applied only locally to small pieces of the system rather than the entire system as a whole. Our procedure exploits the observation that, in practice, the form of modular proofs can be restricted to a very limited set. For completeness, our technique falls back on a non-compositional counterexample search. Using our new procedure, we have solved a number of challenging published examples, including: a 3-D model of the mammalian epidermis; a model of metabolic networks operating in type-2 diabetes; a model of fate determination of vulval precursor cells in the C. elegans worm; and a model of pair-rule regulation during segmentation in the Drosophila embryo. Our results show many orders of magnitude speedup in cases where previous stabilization proving techniques were known to succeed, and new results in cases where tools had previously failed.

Byron Cook, Jasmin Fisher, Elzbieta Krepska, Nir Piterman

Precondition Inference from Intermittent Assertions and Application to Contracts on Collections

Abstract

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 definitely leads to an assertion violation (e.g., for separate static analysis). We define precisely and formally the contract inference problem from intermittent assertions inserted in the code by the programmer. Our definition 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 abstract 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.

Patrick Cousot, Radhia Cousot, Francesco Logozzo

Strengthening Induction-Based Race Checking with Lightweight Static Analysis

Abstract

Direct Memory Access (DMA) is key to achieving high performance in system-level software for multicore processors such as the Cell Broadband Engine. Incorrectly orchestrated DMAs cause DMA races, leading to subtle bugs that are hard to reproduce and fix. In previous work, we have shown that k-induction yields an effective method for proving absence of a restricted class of DMA races. We extend this work to handle a larger class of DMA races. We show that the applicability of k-induction can be significantly improved when combined with three inexpensive static analyses: 1) abstract-interpretation-based static analysis; 2) chunking, a domain-specific invariant generation technique; and 3) code transformations based on statement independence. Our techniques are implemented in the SCRATCH tool. We evaluate our work on industrial benchmarks.

Alastair F. Donaldson, Leopold Haller, Daniel Kroening

Access Nets: Modeling Access to Physical Spaces

Abstract

Electronic, software-managed mechanisms using, for example, radio-frequency identification (RFID) cards, enable great flexibility in specifying access control policies to physical spaces. For example, access rights may vary based on time of day or could differ in normal versus emergency situations. With such fine-grained control, understanding and reasoning about what a policy permits becomes surprisingly difficult requiring knowledge of permission levels, spatial layout, and time. In this paper, we present a formal modeling framework, called AccessNets, suitable for describing a combination of access permissions, physical spaces, and temporal constraints. Furthermore, we provide evidence that model checking techniques are effective in reasoning about physical access control policies. We describe our results from a tool that uses reachability analysis to validate security policies.

Robert Frohardt, Bor-Yuh Evan Chang, Sriram Sankaranarayanan

Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation

Abstract

Dynamic Pushdown Networks (DPNs) are a model for parallel programs with (recursive) procedures and dynamic process creation. Constraints on the sequences of spawned processes allow to extend the basic model with joining of created processes [2]. Orthogonally DPNs can be extended with nested locking [9]. Reachability of a regular set R of configurations in presence of stable constraints as well as reachability without constraints but with nested locking are based on computing the set of predecessors pre ^*(R). In the present paper, we present a forward-propagating algorithm for deciding reachability for DPNs. We represent sets of executions by sets of execution trees and show that the set of all execution trees resulting in configurations from R which either allow a lock-sensitive execution or a join-sensitive execution, is regular. Here, we rely on basic results about macro tree transducers. As a second contribution, we show that reachability is decidable also for DPNs with both nested locking and joins.

Thomas Martin Gawlitza, Peter Lammich, Markus Müller-Olm, Helmut Seidl, Alexander Wenner

Verifying Deadlock-Freedom of Communication Fabrics

Abstract

Avoiding message dependent deadlocks in communication fabrics is critical for modern microarchitectures. If discovered late in the design cycle, deadlocks lead to missed project deadlines and suboptimal design decisions. One approach to avoid this problem is to get high level of confidence on an early microarchitectural model. However, formal proofs of liveness even on abstract models are hard due to large number of queues and distributed control. In this work we address liveness verification of communication fabrics described in the form of high-level microarchitectural models which use a small set of well-defined primitives. We prove that under certain realistic restrictions, deadlock freedom can be reduced to unsatisfiability of a system of Boolean equations. Using this approach, we have automatically verified liveness of several non-trivial models (derived from industrial microarchitectures), where state-of-the-art model checkers failed and pen and paper proofs were either tedious or unknown.

Alexander Gotmanov, Satrajit Chatterjee, Michael Kishinevsky

Static Analysis of Finite Precision Computations

Abstract

We define several abstract semantics for the static analysis of finite precision computations, that bound not only the ranges of values taken by numerical variables of a program, but also the difference with the result of the same sequence of operations in an idealized real number semantics. These domains point out with more or less detail (control point, block, function for instance) sources of numerical errors in the program and the way they were propagated by further computations, thus allowing to evaluate not only the rounding error, but also sensitivity to inputs or parameters of the program. We describe two classes of abstractions, a non relational one based on intervals, and a weakly relational one based on parametrized zonotopic abstract domains called affine sets, especially well suited for sensitivity analysis and test generation. These abstract domains are implemented in the Fluctuat static analyzer, and we finally present some experiments.

Eric Goubault, Sylvie Putot

An Evaluation of Automata Algorithms for String Analysis

Abstract

There has been significant recent interest in automated reasoning techniques, in particular constraint solvers, for string variables. These techniques support a wide variety of clients, ranging from static analysis to automated testing. The majority of string constraint solvers rely on finite automata to support regular expression constraints. For these approaches, performance depends critically on fast automata operations such as intersection, complementation, and determinization. Existing work in this area has not yet provided conclusive results as to which core algorithms and data structures work best in practice.

In this paper, we study a comprehensive set of algorithms and data structures for performing fast automata operations. Our goal is to provide an apples-to-apples comparison between techniques that are used in current tools. To achieve this, we re-implemented a number of existing techniques. We use an established set of regular expressions benchmarks as an indicative workload. We also include several techniques that, to the best of our knowledge, have not yet been used for string constraint solving. Our results show that there is a substantial performance difference across techniques, which has implications for future tool design.

Pieter Hooimeijer, Margus Veanes

Automata Learning with Automated Alphabet Abstraction Refinement

Abstract

Abstraction is the key when learning behavioral models of realistic systems, but also the cause of a major problem: the introduction of non-determinism. In this paper, we introduce a method for refining a given abstraction to automatically regain a deterministic behavior on-the-fly during the learning process. Thus the control over abstraction becomes part of the learning process, with the effect that detected non-determinism does not lead to failure, but to a dynamic alphabet abstraction refinement. Like automata learning itself, this method in general is neither sound nor complete, but it also enjoys similar convergence properties even for infinite systems as long as the concrete system itself behaves deterministically, as illustrated along a concrete example.

Falk Howar, Bernhard Steffen, Maik Merten

Towards Complete Reasoning about Axiomatic Specifications

Abstract

To support verification of expressive properties of functional programs, we consider algebraic style specifications that may relate multiple user-defined functions, and compare multiple invocations of a function for different arguments. We present decision procedures for reasoning about such universally quantified properties of functional programs, using local theory extension methodology. We establish new classes of universally quantified formulas whose satisfiability can be checked in a complete way by finite quantifier instantiation. These classes include single-invocation axioms that generalize standard function contracts, but also certain many-invocation axioms, specifying that functions satisfy congruence, injectivity, or monotonicity with respect to abstraction functions, as well as conjunctions of some of these properties. These many-invocation axioms can specify correctness of abstract data type implementations as well as certain information-flow properties. We also present a decidability-preserving construction that enables the same function to be specified using different classes of decidable specifications on different partitions of its domain.

Swen Jacobs, Viktor Kuncak

String Analysis as an Abstract Interpretation

Abstract

We formalize a string analysis within abstract interpretation framework. The abstraction of strings is given as a conjunction of predicates that describes the common configuration changes on the reference pushdown automaton while processing the strings. We also present a family of pushdown automata called ε bounded pushdown automata. This family covers all context-free languages, and by using this family of pushdown automata, we can prevent abstract values from becoming infinite conjunctions and guarantee that the operations required in the analyzer are computable.

Se-Won Kim, Kwang-Moo Choe

ExplainHoudini: Making Houdini Inference Transparent

Abstract

Houdini is a simple yet scalable technique for annotation inference for modular contract checking. The input to Houdini is a set of candidate annotations, and the output is a consistent subset of these candidates. Since this technique is most useful as an annotation assistant for user-guided refinement of annotations, understanding the reason for the removal of annotations is crucial for a user to refine the set of annotations, and classify false errors easily. This is especially true for applying Houdini to large legacy modules with thousands of procedures and deep call chains. In this work we present a method ExplainHoudini that explains the reason why a given candidate was removed, purely in terms of the existing candidates. We have implemented this algorithm and provide preliminary experience of applying it on large modules.

Shuvendu K. Lahiri, Julien Vanegue

Abstract Probabilistic Automata

Abstract

Probabilistic Automata (PAs) are a widely-recognized mathematical framework for the specification and analysis of systems with non-deterministic and stochastic behaviors. This paper proposes Abstract Probabilistic Automata (APAs), that is a novel abstraction model for PAs. In APAs uncertainty of the non-deterministic choices is modeled by may/must modalities on transitions while uncertainty of the stochastic behaviour is expressed by (underspecified) stochastic constraints. We have developed a complete abstraction theory for PAs, and also propose the first specification theory for them. Our theory supports both satisfaction and refinement operators, together with classical stepwise design operators. In addition, we study the link between specification theories and abstraction in avoiding the state-space explosion problem.

Benoît Delahaye, Joost-Pieter Katoen, Kim G. Larsen, Axel Legay, Mikkel L. Pedersen, Falak Sher, Andrzej Wąsowski

Distributed and Predictable Software Model Checking

Abstract

We present a predicate abstraction and refinement-based algorithm for software verification that is designed for the distributed execution on compute nodes that communicate via message passing, as found in today’s compute clusters. A successful adaptation of predicate abstraction and refinement from sequential to distributed setting needs to address challenges imposed by the inherent non-determinism present in distributed computing environments. In fact, our experiments show that up to an order of magnitude variation of the running time is common when a naive distribution scheme is applied, often resulting in significantly worse running time than the non-distributed version. We present an algorithm that overcomes this pitfall by making deterministic the counterexample selection in spite of the distribution, and still efficiently exploits distributed computational resources. We demonstrate that our distributed software verification algorithm is practical by an experimental evaluation on a set of difficult benchmark problems from the transportation domain.

Nuno P. Lopes, Andrey Rybalchenko

Access Analysis-Based Tight Localization of Abstract Memories

Abstract

On-the-fly localization of abstract memory states is vital for economical abstract interpretation of imperative programs. Such localization is sometimes called “abstract garbage collection” or “framing”. In this article we present a new memory localization technique that is more effective than the conventional reachability-based approach. Our technique is based on a key observation that collecting the reachable memory parts is too conservative and the accessed parts are usually tiny subsets of the reachable. Our technique first estimates, by an efficient pre-analysis, the set of locations that will be accessed during the analysis of each code block. Then the main analysis uses the access-set results to trim the memory entries before analyzing code blocks. In experiments with an industrial-strength global C static analyzer, the technique is applied right before analyzing each procedure’s body and reduces the average analysis time and memory by 92.1% and 71.2%, respectively, without sacrificing the analysis precision. Localizing more frequently such as at loop bodies and basic blocks as well as procedure bodies, the generalized localization additionally reduces analysis time by an average of 31.8%.

Hakjoo Oh, Lucas Brutschy, Kwangkeun Yi

Decision Procedures for Automating Termination Proofs

Abstract

Automated termination provers often use the following schema to prove that a program terminates: construct a relational abstraction of the program’s transition relation and then show that the relational abstraction is well-founded. The focus of current tools has been on developing sophisticated techniques for constructing the abstractions while relying on known decidable logics (such as linear arithmetic) to express them. We believe we can significantly increase the class of programs that are amenable to automated termination proofs by identifying more expressive decidable logics for reasoning about well-founded relations. We therefore present a new decision procedure for reasoning about multiset orderings, which are among the most powerful orderings used to prove termination. We show that, using our decision procedure, one can automatically prove termination of natural abstractions of programs.

Ruzica Piskac, Thomas Wies

Collective Assertions

Abstract

We introduce the notion of collective assertions for message-passing-based parallel programs with distributed memory, such as those written using the Message Passing Interface. A single collective assertion comprises a set of locations in each process and an expression on the global state. The semantics are defined as follows: whenever control in a process reaches one of the locations, a “snapshot”of the local state of that process is sent to a coordinator; once a snapshot has been received from each process, the expression is evaluated on the global state formed by uniting the snapshots. We have extended the Toolkit for Accurate Scientific Software (TASS), a verifier based on symbolic execution and explicit state enumeration, to check that collective assertions hold on all possible executions of a C/MPI program. We give several examples of such programs, show that many properties of them are naturally expressed as collective assertions, and use TASS to verify or refute these.

Stephen F. Siegel, Timothy K. Zirkel

Sets with Cardinality Constraints in Satisfiability Modulo Theories

Abstract

Boolean Algebra with Presburger Arithmetic (BAPA) is a decidable logic that can express constraints on sets of elements and their cardinalities. Problems from verification of complex properties of software often contain fragments that belong to quantifier-free BAPA (QFBAPA). In contrast to many other NP-complete problems (such as quantifier-free first-order logic or linear arithmetic), the applications of QFBAPA to a broader set of problems has so far been hindered by the lack of an efficient implementation that can be used alongside other efficient decision procedures. We overcome these limitations by extending the efficient SMT solver Z3 with the ability to reason about cardinality (QFBAPA) constraints. Our implementation uses the DPLL(T) mechanism of Z3 to reason about the top-level propositional structure of a QFBAPA formula, improving the efficiency compared to previous implementations. Moreover, we present a new algorithm for automatically decomposing QFBAPA formulas. Our algorithm alleviates the exponential explosion of considering all Venn regions, significantly improving the tractability of formulas with many set variables. Because it is implemented as a theory plugin, our implementation enables Z3 to prove formulas that use QFBAPA constructs with constructs from other theories that Z3 supports, as well as with quantifiers. We have applied our implementation to the verification of functional programs; we show it can automatically prove formulas that no automated approach was reported to be able to prove before.

Philippe Suter, Robin Steiger, Viktor Kuncak

Backmatter