Computer Aided Verification

The JSCert project provides a Coq mechanised specification of the core JavaScript language. A key part of the project was to develop a methodology for establishing trust, by designing JSCert in such a way as to provide a strong connection with the JavaScript standard, and by developing JSRef, a reference interpreter which was proved correct with respect to JSCert and tested using the standard Test262 test suite. In this paper, we assess the previous state of the project at POPL’14 and the current state of the project at CAV’15. We evaluate the work of POPL’14, providing an analysis of the methodology as a whole and a more detailed analysis of the tests. We also describe recent work on extending JSRef to include Google’s V8 Array library, enabling us to cover more of the language and to pass more tests.

In this paper we introduce the first known fully automated tool for symbolically proving

CTL

$$^*$$

properties of (infinite-state) integer programs. The method uses an internal encoding which facilitates reasoning about the subtle interplay between the nesting of path and state temporal operators that occurs within

CTL

$$^*$$

proofs. A precondition synthesis strategy is then used over a program transformation which trades nondeterminism in the transition relation for nondeterminism explicit in variables predicting future outcomes when necessary. We show the viability of our approach in practice using examples drawn from device drivers and various industrial examples.

We present an automata-based algorithm for checking finite state systems for hyperproperties specified in HyperLTL and HyperCTL

$$^*$$

. For the alternation-free fragments of HyperLTL and HyperCTL

$$^*$$

the automaton construction allows us to leverage existing model checking technology. Along several case studies, we demonstrate that the approach enables the verification of real hardware designs for properties that could not be checked before. We study information flow properties of an I2C bus master, the symmetric access to a shared resource in a mutual exclusion protocol, and the functional correctness of encoders and decoders for error resistant codes.

The construction of a proof for unsatisfiability is less costly than the construction of a ranking function. We present a new approach to LTL software model checking (i.e., to statically analyze a program and verify a temporal property from the full class of LTL including general liveness properties) which aims at exploiting this fact. The idea is to select finite prefixes of a path and check these for infeasibility before considering the full infinite path. We have implemented a tool which demonstrates the practical potential of the approach. In particular, the tool can verify several benchmark programs for a liveness property just with finite prefixes (and thus without the construction of a single ranking function).

We characterize the complexity of liveness verification for parameterized systems consisting of a leader process and arbitrarily many anonymous and identical contributor processes. Processes communicate through a shared, bounded-value register. While each operation on the register is atomic, there is no synchronization primitive to execute a sequence of operations atomically.

We analyze the case in which processes are modeled by finite-state machines or pushdown machines and the property is given by a Büchi automaton over the alphabet of read and write actions of the leader. We show that the problem is decidable, and has a surprisingly low complexity: it is NP-complete when all processes are finite-state machines, and is PSPACE-hard and in NEXPTIME when they are pushdown machines. This complexity is lower than for the non-parameterized case: liveness verification of finitely many finite-state machines is PSPACE-complete, and undecidable for two pushdown machines.

For finite-state machines, our proofs characterize infinite behaviors using existential abstraction and semilinear constraints. For pushdown machines, we show how contributor computations of high stack height can be simulated by computations of many contributors, each with low stack height. Together, our results characterize the complexity of verification for parameterized systems under the assumptions of anonymity and asynchrony.

Automatic verification of threshold-based fault-tolerant distributed algorithms (FTDA) is challenging: they have multiple parameters that are restricted by arithmetic conditions, the number of processes and faults is parameterized, and the algorithm code is parameterized due to conditions counting the number of received messages. Recently, we introduced a technique that first applies data and counter abstraction and then runs bounded model checking (BMC). Given an FTDA, our technique computes an upper bound on the diameter of the system. This makes BMC complete: it always finds a counterexample, if there is an actual error. To verify state-of-the-art FTDAs, further improvement is needed. In this paper, we encode bounded executions over integer counters in SMT. We introduce a new form of offline partial order reduction that exploits acceleration and the structure of the FTDAs. This aggressively prunes the execution space to be explored by the solver. In this way, we verified safety of seven FTDAs that were out of reach before.

We introduce skipping refinement, a new notion of correctness for reasoning about optimized reactive systems. Reasoning about reactive systems using refinement involves defining an abstract, high-level

specification

system and a concrete, low-level

implementation

system. One then shows that every behavior allowed by the implementation is also allowed by the specification. Due to the difference in abstraction levels, it is often the case that the implementation requires many steps to match one step of the specification, hence, it is quite useful for refinement to directly account for

stuttering

. Some optimized implementations, however, can actually take multiple specification steps at once. For example, a memory controller can buffer the commands to the memory and at a later time simultaneously update multiple memory locations, thereby

skipping

several observable states of the abstract specification, which only updates one memory location at a time. We introduce skipping simulation refinement and provide a sound and complete characterization consisting of “local” proof rules that are amenable to mechanization and automated verification. We present case studies that highlight the applicability of skipping refinement: a JVM-inspired stack machine, a simple memory controller and a scalar to vector compiler transformation. Our experimental results demonstrate that current model-checking and automated theorem proving tools have difficulty automatically analyzing these systems using existing notions of correctness, but they can analyze the systems if we use skipping refinement.

Markov decision processes (MDPs) with multi-dimensional weights are useful to analyze systems with multiple objectives that may be conflicting and require the analysis of trade-offs. In this paper, we study the complexity of percentile queries in such MDPs and give algorithms to synthesize strategies that enforce such constraints. Given a multi-dimensional weighted MDP and a quantitative payoff function

f

, thresholds

$$v_i$$

(one per dimension), and probability thresholds

$$\alpha _i$$

, we show how to compute a single strategy to enforce that for all dimensions

i

, the probability of outcomes

$$\rho $$

satisfying

$$f_i(\rho ) \ge v_i$$

is at least

$$\alpha _i$$

. We consider classical quantitative payoffs from the literature (sup, inf, lim sup, lim inf, mean-payoff, truncated sum, discounted sum). Our work extends to the quantitative case the multi-objective model checking problem studied by Etessami et al. [

16

] in unweighted MDPs.

We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean-payoff property, the ratio property, and the minimum initial credit for energy property. The algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with constant treewidth, and it is well-known that the control-flow graphs of most programs have constant treewidth. Let

n

denote the number of nodes of a graph,

m

the number of edges (for constant treewidth graphs

$$m=O(n)$$

) and

W

the largest absolute value of the weights. Our main theoretical results are as follows. First, for constant treewidth graphs we present an algorithm that approximates the mean-payoff value within a multiplicative factor of

$$\epsilon $$

in time

$$O(n \cdot \log (n/\epsilon ))$$

and linear space, as compared to the classical algorithms that require quadratic time. Second, for the ratio property we present an algorithm that for constant treewidth graphs works in time

$$O(n \cdot \log (|a\cdot b|))=O(n\cdot \log (n\cdot W))$$

, when the output is

$$\frac{a}{b}$$

, as compared to the previously best known algorithm with running time

$$O(n^2 \cdot \log (n\cdot W))$$

. Third, for the minimum initial credit problem we show that (i) for general graphs the problem can be solved in

$$O(n^2\cdot m)$$

time and the associated decision problem can be solved in

$$O(n\cdot m)$$

time, improving the previous known

$$O(n^3\cdot m\cdot \log (n\cdot W))$$

and

$$O(n^2 \cdot m)$$

bounds, respectively; and (ii) for constant treewidth graphs we present an algorithm that requires

$$O(n\cdot \log n)$$

time, improving the previous known

$$O(n^4 \cdot \log (n \cdot W))$$

bound. We have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks.

For deterministic systems, a counterexample to a property can simply be an error trace, whereas counterexamples in probabilistic systems are necessarily more complex. For instance, a set of erroneous traces with a sufficient cumulative probability mass can be used. Since these are too large objects to understand and manipulate, compact representations such as subchains have been considered. In the case of probabilistic systems with non-determinism, the situation is even more complex. While a subchain for a given strategy (or scheduler, resolving non-determinism) is a straightforward choice, we take a different approach. Instead, we focus on the strategy itself, and extract the most important decisions it makes, and present its succinct representation.

The key tools we employ to achieve this are (1) introducing a concept of importance of a state w.r.t. the strategy, and (2) learning using decision trees. There are three main consequent advantages of our approach. Firstly, it exploits the quantitative information on states, stressing the more important decisions. Secondly, it leads to a greater variability and degree of freedom in representing the strategies. Thirdly, the representation uses a self-explanatory data structure. In summary, our approach produces more succinct and more explainable strategies, as opposed to e.g. binary decision diagrams. Finally, our experimental results show that we can extract several rules describing the strategy even for very large systems that do not fit in memory, and based on the rules explain the erroneous behaviour.

Proving quantitative properties of programs, such as bounds on resource usage or information leakage, often leads to verification conditions that involve cardinalities of sets. Existing approaches for dealing with such verification conditions operate by checking cardinality bounds for given formulas. However, they cannot synthesize formulas that satisfy given cardinality constraints, which limits their applicability for inferring cardinality-based inductive arguments.

In this paper we present an algorithm for synthesizing formulas for given cardinality constraints, which relies on the theory of counting integer points in symbolic polytopes. We cast our algorithm in terms of a cardinality-constrained interpolation procedure, which we put to work in a solver for recursive Horn clauses with cardinality constraints based on abstraction refinement. We implement our technique and describe its evaluation on a number of representative examples.

Quantitative analysis of Markov models typically proceeds through numerical methods or simulation-based evaluation. Since the state space of the models can often be large, exact or approximate state aggregation methods (such as lumping or bisimulation reduction) have been proposed to improve the scalability of the numerical schemes. However, none of the existing numerical techniques provides general, explicit bounds on the approximation error, a problem particularly relevant when the level of accuracy affects the soundness of verification results. We propose a novel numerical approach that combines the strengths of aggregation techniques (state-space reduction) with those of simulation-based approaches (automatic updates that adapt to the process dynamics). The key advantage of our scheme is that it provides rigorous precision guarantees under different measures. The new approach, which can be used in conjunction with time uniformisation techniques, is evaluated on two models of chemical reaction networks, a signalling pathway and a prokaryotic gene expression network: it demonstrates marked improvement in accuracy without performance degradation, particularly when compared to known state-space truncation techniques.

We present PROPhESY, a tool for analyzing parametric Markov chains (MCs). It can compute a rational function (i.e., a fraction of two polynomials in the model parameters) for reachability and expected reward objectives. Our tool outperforms state-of-the-art tools and supports the novel feature of conditional probabilities. PROPhESY supports incremental automatic parameter synthesis (using SMT techniques) to determine “safe” and “unsafe” regions of the parameter space. All values in these regions give rise to instantiated MCs satisfying or violating the (conditional) probability or expected reward objective. PROPhESY features a web front-end supporting visualization and user-guided parameter synthesis. Experimental results show that PROPhESY scales to MCs with millions of states and several parameters.

In recent years, string solvers have become an essential component in many formal-verification, security-analysis and bug-finding tools. Such solvers typically support a theory of string equations, the length function as well as the regular-expression membership predicate. These enable considerable expressive power, which comes at the cost of slow solving time, and in some cases even nontermination. We present two techniques, designed for word-based SMT string solvers, to mitigate these problems: (i) sound and complete detection of overlapping variables, which is essential to avoiding common cases of nontermination; and (ii) pruning of the search space via bi-directional integration between the string and integer theories, enabling new cross-domain heuristics. We have implemented both techniques atop the Z3-str solver, resulting in a significantly more robust and efficient solver, dubbed Z3str2, for the quantifier-free theory of string equations, the regular-expression membership predicate and linear arithmetic over the length function. We report on a series of experiments over four sets of challenging real-world benchmarks, where we compared Z3str2 with five different string solvers: S3, CVC4, Kaluza, PISA and Stranger. Each of these tools utilizes a different solving strategy and/or string representation (based e.g. on words, bit vectors or automata). The results point to the efficacy of our proposed techniques, which yield dramatic performance improvement. We argue that the techniques presented here are of broad applicability, and can be integrated into other SMT-backed string solvers to improve their performance.

Most common vulnerabilities in Web applications are due to string manipulation errors in input validation and sanitization code. String constraint solvers are essential components of program analysis techniques for detecting and repairing vulnerabilities that are due to string manipulation errors. For quantitative and probabilistic program analyses, checking the satisfiability of a constraint is not sufficient, and it is necessary to count the number of solutions. In this paper, we present a constraint solver that, given a string constraint, (1) constructs an automaton that accepts all solutions that satisfy the constraint, (2) generates a function that, given a length bound, gives the total number of solutions within that bound. Our approach relies on the observation that, using an automata-based constraint representation, model counting reduces to path counting, which can be solved precisely. We demonstrate the effectiveness of our approach on a large set of string constraints extracted from real-world web applications.

We investigate the correctness of TimSort, which is the main sorting algorithm provided by the Java standard library. The goal is functional verification with mechanical proofs. During our verification attempt we discovered a bug which causes the implementation to crash. We characterize the conditions under which the bug occurs, and from this we derive a bug-free version that does not compromise the performance. We formally specify the new version and mechanically verify the absence of this bug with KeY, a state-of-the-art verification tool for Java.

In

runtime verification

, the central problem is to decide if a given program execution violates a given property. In

online

runtime verification, a monitor observes a program’s execution as it happens. If the program being observed has hard real-time constraints, then the monitor inherits them. In the presence of hard real-time constraints it becomes a challenge to maintain enough information to produce

error traces

, should a property violation be observed. In this paper we introduce a data structure, called

tree buffer

, that solves this problem in the context of automata-based monitors: If the monitor itself respects hard real-time constraints, then enriching it by tree buffers makes it possible to provide error traces, which are essential for diagnosing defects. We show that tree buffers are also useful in other application domains. For example, they can be used to implement functionality of

capturing groups

in regular expressions. We prove optimal asymptotic bounds for our data structure, and validate them using empirical data from two sources: regular expression searching through Wikipedia, and runtime verification of execution traces obtained from the DaCapo test suite.

In this work we present a new sampling-based “black box” inference approach for learning the behaviors of a library component. As an application, we focus on the problem of automatically learning

commutativity specifications

of data structures. This is a very challenging problem, yet important, as commutativity specifications are fundamental to program analysis, concurrency control and even lower bounds.

Our approach is enabled by three core insights: (i)

type-aware sampling

which drastically improves the quality of obtained examples, (ii)

relevant predicate discovery

critical for reducing the formula search space, and (iii) an

efficient search

based on weighted-set cover for finding formulas ranging over the predicates and capturing the examples.

More generally, our work learns formulas belonging to fragments consisting of quantifier-free formulas over a finite number of relation symbols. Such fragments are expressive enough to capture useful specifications (e.g., commutativity) yet are amenable to automated inference.

We implemented a tool based on our approach and have shown that it can quickly learn non-trivial and important commutativity specifications of fundamental data types such as hash maps, sets, array lists, union find and others. We also showed experimentally that learning these specifications is beyond the capabilities of existing techniques.

Verification of open programs can be challenging in the presence of an unconstrained environment. Verifying properties that depend on the environment yields a large class of uninteresting false alarms. Using a verifier on a program thus requires extensive initial investment in modeling the environment of the program. We propose a technique called

angelic verification

for verification of open programs, where we constrain a verifier to report warnings only when no acceptable environment specification exists to prove the assertion. Our framework is parametric in a vocabulary and a set of angelic assertions that allows a user to configure the tool. We describe a few instantiations of the framework and an evaluation on a set of real-world benchmarks to show that our technique is competitive with industrial-strength tools even without models of the environment.

In this paper, we present

SeaHorn

, a software verification framework. The key distinguishing feature of

SeaHorn

is its modular design that separates the concerns of the syntax of the programming language, its operational semantics, and the verification semantics.

SeaHorn

encompasses several novelties: it (a) encodes verification conditions using an efficient yet precise inter-procedural technique, (b) provides flexibility in the verification semantics to allow different levels of precision, (c) leverages the state-of-the-art in software model checking and abstract interpretation for verification, and (d) uses Horn-clauses as an intermediate language to represent verification conditions which simplifies interfacing with multiple verification tools based on Horn-clauses.

SeaHorn

provides users with a powerful verification tool and researchers with an extensible and customizable framework for experimenting with new software verification techniques. The effectiveness and scalability of

SeaHorn

are demonstrated by an extensive experimental evaluation using benchmarks from SV-COMP 2015 and real avionics code.

Equivalence checking of imperative programs has several applications including compiler validation and cross-version verification. Debugging equivalence failures can be tedious for large examples, especially for low-level binary programs. In this paper, we formalize a simple yet precise notion of

verifiable rootcause

for equivalence failures that leverages semantic similarity between two programs. Unlike existing works on program repair, our definition of rootcause avoids the need for a template of fixes or the need for a complete repair to ensure equivalence. We show progressively weaker checks for detecting rootcauses that can be applicable even when multiple fixes are required to make the two programs equivalent. We provide optimizations based on Maximum Satisfiability (MAXSAT) and binary search to prune the search space of such rootcauses. We have implemented the techniques in SymDiff and provide an evaluation on a set of real-world compiler validation binary benchmarks.

Developing provably correct programs is an incremental process that often involves a series of interactions with a program verifier. To increase the responsiveness of the program verifier during such interactions, we designed a system for fine-grained caching of verification results. The caching system uses the program’s call graph and control-flow graph to focus the verification effort on just the parts of the program that were affected by the user’s most recent modifications. The novelty lies in how the original program is instrumented with cached information to avoid unnecessary work for the verifier. The system has been implemented in the Boogie verification engine, which allows it to be used by different verification front ends that target the intermediate verification language Boogie; we present one such application in the integrated development environment for the Dafny programming language. The paper describes the architecture and algorithms of the caching system and reports on how much it improves the performance of the verifier in practice.

We study the problem of efficiently predicting a correct program from a large set of programs induced from few input-output examples in Programming-by-Example (PBE) systems.

The inference and the verification of numerical relationships among variables of a program is one of the main goals of static analysis. In this paper, we propose an Abstract Interpretation framework based on higher-dimensional ellipsoids to automatically discover symbolic quadratic invariants within loops, using loop counters as implicit parameters. In order to obtain non-trivial invariants, the diameter of the set of values taken by the numerical variables of the program has to evolve (sub-)linearly during loop iterations. These invariants are called ellipsoidal cones and can be seen as an extension of constructs used in the static analysis of digital filters. Semidefinite programming is used to both compute the numerical results of the domain operations and provide proofs (witnesses) of their correctness.

We present

Adam

, a tool for the automatic synthesis of distributed systems with multiple concurrent processes. For each process, an individual controller is synthesized that acts on locally available information obtained through synchronization with the environment and with other system processes.

Adam

is based on Petri games, an extension of Petri nets where each token is a player in a multiplayer game.

Adam

implements the first symbolic game solving algorithm for Petri games. We report on experience from several case studies with up to 38 system processes.

We present a technique and an accompanying tool that learns guarded affine functions. In our setting, a teacher starts with a guarded affine function and the learner learns this function using equivalence queries only. In each round, the teacher examines the current hypothesis of the learner and gives a counter-example in terms of an input-output pair where the hypothesis differs from the target function. The learner uses these input-output pairs to learn the guarded affine expression. This problem is relevant in synthesis domains where we are trying to synthesize guarded affine functions that have particular properties, provided we can build a teacher who can answer using such counter-examples. We implement our approach and show that our learner is effective in learning guarded affine expressions, and more effective than general-purpose synthesis techniques.

Many SMT problems of interest may require the capability of finding models that are

optimal

wrt. some objective functions. These problems are grouped under the umbrella term of

Optimization Modulo Theories – OMT

. In this paper we present

OptiMathSAT

, an OMT tool extending the

MathSAT5

SMT solver.

OptiMathSAT

allows for solving a list of optimization problems on SMT formulas with linear objective functions –on the Boolean, the rational and the integer domains, and on their combination thereof– including MaxSMT. Multiple objective functions can be combined together and handled either independently, or lexicographically, or in a min-max/max-min fashion.

OptiMathSAT

ships with an extended SMT-LIBV2 input syntax and C API bindings, and it preserves the incremental attitude of its underlying SMT solver.

Smartphone and tablet “apps” are particularly susceptible to asynchrony bugs. In order to maintain responsive user interfaces, events are handled asynchronously. Unexpected schedules of event handlers can result in apparently-random bugs which are notoriously difficult to reproduce, even given the user-event sequences that trigger them.

We develop the AsyncDroid tool for the systematic discovery and reproduction of asynchrony bugs in Android apps. Given an app and a user-event sequence, AsyncDroid systematically executes alternate schedules of the same asynchronous event handlers, according to a programmable schedule enumerator. The input user-event sequence is given either by user interaction, or can be generated by automated

ui

“monkeys”. By exposing and controlling the factors which influence the scheduling order of asynchronous handlers, our programmable enumerators can explicate reproducible schedules harboring bugs. By enumerating all schedules within a limited threshold of reordering, we maximize the likelihood of encountering asynchrony bugs, according to prevailing hypotheses in the literature, and discover several bugs in Android apps found in the wild.

We present version 1.0 of the Norn SMT solver for string constraints. Norn is a solver for an expressive constraint language, including word equations, length constraints, and regular membership queries. As a feature distinguishing Norn from other SMT solvers, Norn is a decision procedure under the assumption of a set of acyclicity conditions on word equations, without any restrictions on the use of regular membership.

PVSio-web is a graphical environment for facilitating the design and evaluation of interactive (human-computer) systems. Using PVSio-web, one can generate and evaluate realistic interactive prototypes from formal models. PVSio-web has been successfully used over the last two years for analyzing commercial, safety-critical medical devices. It has been used to create training material for device developers and device users. It has also been used for medical device design, by both formal methods experts and non-technical end users.

This paper presents the latest release of PVSio-web 2.0, which will be part of the next PVS distribution. The new tool architecture is discussed, and the rationale behind its design choices are presented.

PVSio-web Tool:

http://www.pvsioweb.org

We propose a flexible exchange format for

$$\omega $$

-automata, as typically used in formal verification, and implement support for it in a range of established tools. Our aim is to simplify the interaction of tools, helping the research community to build upon other people’s work. A key feature of the format is the use of very generic acceptance conditions, specified by Boolean combinations of acceptance primitives, rather than being limited to common cases such as Büchi, Streett, or Rabin. Such flexibility in the choice of acceptance conditions can be exploited in applications, for example in probabilistic model checking, and furthermore encourages the development of acceptance-agnostic tools for automata manipulations. The format allows acceptance conditions that are either state-based or transition-based, and also supports alternating automata.

In this paper, we present

LearnLib

, a library for active automata learning. The current, open-source version of

LearnLib

was completely rewritten from scratch, incorporating the lessons learned from the decade-spanning development process of the previous versions of

LearnLib

. Like its immediate predecessor, the open-source

LearnLib

is written in Java to enable a high degree of flexibility and extensibility, while at the same time providing a performance that allows for large-scale applications. Additionally,

LearnLib

provides facilities for visualizing the progress of learning algorithms in detail, thus complementing its applicability in research and industrial contexts with an educational aspect.

A popular model of asynchronous programming consists of a single-threaded worker process interacting with a task queue. In each step of such a program, the worker takes a task from the queue and executes its code atomically to completion. Executing a task can call “normal” functions as well as post additional asynchronous tasks to the queue. Additionally, tasks can be posted to the queue by the environment.

Bouajjani and Emmi introduced

phase-bounding

analysis on asynchronous programs with unbounded FIFO task queues, which is a systematic exploration of all program behaviors up to a fixed

task phase

. They showed that phase-bounded exploration can be sequentialized: given a set of recursive tasks, a task queue, and a phase bound

$$L > 0$$

, one can construct a sequential recursive program whose behaviors capture all states of the original asynchronous program reachable by an execution where only tasks up to phase

L

are executed. However, there was no empirical evaluation of the method.

We describe our tool

Bbs

that implements phase-bounding to analyze embedded C programs generated from TinyOS applications, which are widely used in wireless sensor networks. Our empirical results indicate that a variety of subtle safety-violation bugs are manifested within a small phase bound (3 in most of the cases). While our evaluation focuses on TinyOS, our tool is generic, and can be ported to other platforms that employ a similar programming model.

HybridSal is a tool for enabling verification of hybrid systems using infinite bounded model checking and k-induction. The core component of the tool is an abstraction engine that automatically creates a discrete, but infinite, state transition system abstraction of the continuous dynamics in the system. In this paper, we describe HybridSal’s new capability to create time-aware relational abstractions, which gives users control over the precision of the abstraction. We also describe a novel approach for abstracting nonlinear expressions that allows us to create time-aware relational abstractions that are more precise than those described previously. We show that the new approach enables automatic verification of systems that could not be verified previously.

Developing enterprise software often requires composing several libraries together with a large body of in-house code. Large APIs introduce a steep learning curve for new developers as a result of their complex object-oriented underpinnings. While the written code in general reflects a programmer’s intent, due to evolutions in an API, code can often become ill-typed, yet still syntactically-correct. Such code fragments will no longer compile, and will need to be updated. We describe an algorithm that automatically repairs such errors, and discuss its application to common problems in software engineering.

SAE Aerospace Information Report 6110, “Contiguous Aircraft/System Development Process Example,” follows the development of a complex wheel brake system (WBS) using processes in the industry standards

Arp4754A

, “Guidelines for Development of Civil Aircraft and Systems,” and

Arp4761

, “Guidelines and Methods for Conducting the Safety Assessment Process on Civil Airborne Systems and Equipment.”

Air6110

employs informal methods to examine several WBS architectures which meet the same requirements with different degrees of reliability.

In this case study, we analyze the

Air6110

with formal methods. First, WBS architectures in

Air6110

formerly using informal steps are recreated in a formal manner. Second, methods to automatically analyze and compare the behaviors of various architectures with additional, complementary information not included in the

Air6110

are presented. Third, we provide an assessment of distinct formal methods ranging from contract-based design, to model checking, to model based safety analysis.

We present the verification of a benchmark powertrain control system using the hybrid system verification tool C2E2. This model comes from a suite of benchmarks that were posed as a challenge problem for the hybrid systems community, and to our knowledge, we are reporting its first verification. For this work, we implemented the algorithm reported in [

10

] in C2E2, to automatically compute local discrepancy (rate of convergence or divergence of trajectories) of the model. We verify the key requirements of the model, specified in signal temporal logic (STL), for a set of driver behaviors.

Recent experimental advances in biology allow researchers to obtain gene expression profiles at single-cell resolution over hundreds, or even thousands of cells at once. These single-cell measurements provide snapshots of the states of the cells that make up a tissue, instead of the population-level averages provided by conventional high-throughput experiments. This new data therefore provides an exciting opportunity for computational modelling. In this paper we introduce the idea of viewing single-cell gene expression profiles as states of an asynchronous Boolean network, and frame model inference as the problem of reconstructing a Boolean network from its state space. We then give a scalable algorithm to solve this synthesis problem. We apply our technique to both simulated and real data. We first apply our technique to data simulated from a well established model of common myeloid progenitor differentiation. We show that our technique is able to recover the original Boolean network rules. We then apply our technique to a large dataset taken during embryonic development containing thousands of cell measurements. Our technique synthesises matching Boolean networks, and analysis of these models yields new predictions about blood development which our experimental collaborators were able to verify.

In this paper we study empirical metrics for software source code, which can predict the performance of verification tools on specific types of software. Our metrics comprise variable usage patterns, loop patterns, as well as indicators of control-flow complexity and are extracted by simple data-flow analyses. We demonstrate that our metrics are powerful enough to devise a machine-learning based portfolio solver for software verification. We show that this portfolio solver would be the (hypothetical) overall winner of both the 2014 and 2015 International Competition on Software Verification (SV-COMP). This gives strong empirical evidence for the predictive power of our metrics and demonstrates the viability of portfolio solvers for software verification.

We present

Universal Property Directed Reachability

(

$$\mathsf PDR ^{\forall }$$

), a property-directed procedure for automatic inference of invariants in a universal fragment of first-order logic.

$$\mathsf PDR ^{\forall }$$

is an extension of Bradley’s PDR/IC3 algorithm for inference of propositional invariants.

$$\mathsf PDR ^{\forall }$$

terminates when it either discovers a concrete counterexample, infers an inductive universal invariant strong enough to establish the desired safety property, or finds a

proof that such an invariant does not exist

. We implemented an analyzer based on

$$\mathsf PDR ^{\forall }$$

, and applied it to a collection of list-manipulating programs. Our analyzer was able to automatically infer universal invariants strong enough to establish memory safety and certain functional correctness properties, show the absence of such invariants for certain natural programs and specifications, and detect bugs. All this, without the need for user-supplied abstraction predicates.

Safety analysis investigates system behavior under faulty conditions. It is a fundamental step in the design of complex systems, that is often mandated by certification procedures. Safety analysis includes two key steps: the construction of all minimal cut sets (MCSs) for a given property (i.e. the sets of basic faults that may cause a failure), and the computation of the corresponding probability (given probabilities for the basic faults).

Model-based Safety Analysis relies on formal verification to carry out these tasks. However, the available techniques suffer from scalability problems, and are unable to provide useful results if the computation does not complete.

In this paper, we investigate and evaluate a family of IC3-based algorithms for MCSs computation. We work under the monotonicity assumption of safety analysis (i.e. an additional fault can not prevent the violation of the property). We specialize IC3-based routines for parameter synthesis by optimizing the counterexample generalization, by ordering the exploration of MCSs based on increasing cardinality, and by exploiting the inductive invariants built by IC3 to accelerate convergence.

Other enhancements yield an “anytime” algorithm, able to produce an increasingly precise probability estimate as the discovery of MCSs proceeds, even when the computation does not terminate.

A thorough experimental evaluation clearly demonstrates the substantial advances resulting from the proposed methods.

$$k$$

-induction is a promising technique to extend bounded model checking from falsification to verification. In software verification,

$$k$$

-induction works only if auxiliary invariants are used to strengthen the induction hypothesis. The problem that we address is to generate such invariants (1) automatically without user-interaction, (2) efficiently such that little verification time is spent on the invariant generation, and (3) that are sufficiently strong for a

$$k$$

-induction proof. We boost the

$$k$$

-induction approach to significantly increase effectiveness and efficiency in the following way: We start in parallel to

$$k$$

-induction a data-flow-based invariant generator that supports dynamic precision adjustment and refine the precision of the invariant generator continuously during the analysis, such that the invariants become increasingly stronger. The

$$k$$

-induction engine is extended such that the invariants from the invariant generator are injected in each iteration to strengthen the hypothesis. The new method solves the above-mentioned problem because it (1) automatically chooses an invariant by step-wise refinement, (2) starts always with a lightweight invariant generation that is computationally inexpensive, and (3) refines the invariant precision more and more to inject stronger and stronger invariants into the induction system. We present and evaluate an implementation of our approach, as well as all other existing approaches, in the open-source verification-framework

CPAchecker

. Our experiments show that combining

$$k$$

-induction with continuously-refined invariants significantly increases effectiveness and efficiency, and outperforms all existing implementations of

$$k$$

-induction-based verification of C programs in terms of successful results.

Bounded Model Checking

(BMC) is well known for its simplicity and ability to find counterexamples. It is based on the idea of symbolically representing counterexamples in a transition system and then using a SAT solver to check for their existence or their absence. State-of-the-art BMC algorithms combine a direct translation to SAT with circuit-aware simplifications and work incrementally, sharing information between different bounds. While BMC is incomplete (it can only show existence of counterexamples), it is a major building block of several complete interpolation-based model checking algorithms. However, traditional interpolation is incompatible with optimized BMC. Hence, these algorithms rely on simple BMC engines that significantly hinder their performance. In this paper, we present a Fast Interpolating BMC (

Fib

) that combines state-of-the-art BMC techniques with interpolation. We show how to interpolate in the presence of circuit-aware simplifications and in the context of incremental solving. We evaluate our implementation of

Fib

in AVY, an interpolating property directed model checker, and show that it has a great positive effect on the overall performance. With the

Fib

, AVY outperforms ABC implementation of

Pdr

on both HWMCC’13 and HWMCC’14 benchmarks.

We apply multivariate Lagrange interpolation to synthesizing polynomial quantitative loop invariants for probabilistic programs. We reduce the computation of a quantitative loop invariant to solving constraints over program variables and unknown coefficients. Lagrange interpolation allows us to find constraints with less unknown coefficients. Counterexample-guided refinement furthermore generates linear constraints that pinpoint the desired quantitative invariants. We evaluate our technique by several case studies with polynomial quantitative loop invariants in the experiments.