Hardware and Software: Verification and Testing

Our central result is a proof method that simplifies proofs of linearizability on TSO. This is necessary since the use of local buffers in TSO adds considerably to the verification overhead on top of the already subtle linearizability proofs. The proof method involves constructing a coarse-grained abstraction as an intermediate layer between an abstract description and the concurrent algorithm. This allows the linearizability proof to be split into two smaller components, where the effect of the local buffers in TSO is dealt with at a higher level of abstraction than it would have been otherwise.

A major challenge for processor-level stimuli generators is the need to generate stimuli that exercise deep micro-architectural mechanisms. Advanced generators address this challenge by applying expert testing knowledge that bias the stimuli toward interesting verification events. In this paper, we present a new approach whereby scenarios are not just enhanced, but are actually modified by testing knowledge. By allowing such mutations, scenarios are diverted toward quasi-events that are semantically related, though not identical, to the original intent of the scenario. We describe the importance of quasi-events and the usefulness of automated scenario mutations for improving the verification of speculative execution.

We present a hybrid model checking algorithm for incomplete timed systems where parts of the system are unspecified (so-called black boxes). Here, we answer the question of unrealisability, i.e., “Is there a path violating a safety property regardless of the implementation of the black boxes?” Existing bounded model checking (BMC) approaches for incomplete timed systems exploit the power of modern SMT solvers, but might be too coarse as an abstraction for certain problem instances. On the other hand, symbolic model checking (SMC) for incomplete timed systems is more accurate, but may fail due to the size of the explored state space. In this work, we propose a tight integration of a backward SMC routine with a forward BMC procedure leveraging the strengths of both worlds. The symbolic model checker is hereby used to compute an enlarged target which we then try to hit using BMC. We use learning strategies to guide the SMT solver’s search into the right direction and manipulate the enlarged target to improve the overall accuracy of the current verification run. Our experimental results show that the hybrid approach is able to verify incomplete timed systems which are out of the scope for BMC and can neither be solved in reasonable time using SMC. Furthermore, our approach compares favourably with UPPAAL-TIGA when considering timed games as a special case of the unrealisability problem.

DYNAMATE is a tool that automatically infers loop invariants and uses them to prove Java programs correct with respect to a given JML functional specification. DYNAMATE improves the flexibility of loop invariant inference by integrating static (proving) and dynamic (testing) techniques with the goal of combining their complementary strengths. In an experimental evaluation involving 26 Java methods of java.util annotated with JML pre- and postconditions, it automatically discharged over 97% of all proof obligations, resulting in automatic complete correctness proofs of 23 out of the 26 methods.

We present an algorithm to automatically extract inductive modulo-2 linear invariants from a design. This algorithm makes use of basic linear algebra and is realized on top of an incremental SAT solver. The experimental results demonstrate that a large number of designs possess linear invariants that can be efficiently found by our method. We study how these invariants can be helpful in the contexts of model checking and synthesis.

Boolean controllers for systems with complex datapaths are often very difficult to implement correctly, in particular when concurrency is involved. Yet, in many instances it is easy to formally specify correctness. For example, the specification for the controller of a pipelined processor only has to state that the pipelined processor gives the same results as a non-pipelined reference design. This makes such controllers a good target for automated synthesis. However, an efficient abstraction for the complex datapath elements is needed, as a bit-precise description is often infeasible. We present Suraq, the first controller synthesis tool which uses uninterpreted functions for the abstraction. Quantified first-order formulas (with specific quantifier structure) serve as the specification language from which Suraq synthesizes Boolean controllers. Suraq transforms the specification into an unsatisfiable SMT formula, and uses Craig interpolation to compute its results. Using Suraq, we were able to synthesize a controller (consisting of two Boolean signals) for a five-stage pipelined DLX processor in roughly one hour and 15 minutes.

Java Modeling Language (JML) is a specification language for Java programs, that follows the design by contract paradigm. However, it is not always easy to use JML, for example when specifying properties of linked data structures. Alloy, on the other hand, is a relational specification language with a built-in transitive closure operator, which makes it particularly suitable for writing concise specifications of linked data structures. This paper presents Alloy2JML, a tool that generates JML specifications from Alloy expression, in order to support both Alloy and JML specifications in the KeY verification engine. This translation allows Java programs with Alloy specifications to be fully verified for correctness. Moreover, Alloy2JML lets Alloy specifications be employed in a variety of tools that accept only JML as their specification language. Supporting Alloy has the additional advantage that users can validate the specifications beforehand using the Alloy Analyzer.

Compositional verification techniques in the assume-guarantee style have been successfully applied to transition systems to efficiently reduce the search space by leveraging the compositional nature of the systems under consideration. We adapt these techniques to the domain of hybrid systems with affine dynamics. To build assumptions we introduce an abstraction based on location merging. We integrate the assume-guarantee style analysis with automatic abstraction refinement. We have implemented our approach in the symbolic hybrid model checker SpaceEx. The evaluation shows its practical potential. To the best of our knowledge, this is the first work combining assume-guarantee reasoning with automatic abstraction-refinement in the context of hybrid automata.

Linearizability is the key correctness criterion for concurrent data structures. In recent years, numerous verification techniques for linearizability have been developed, ranging from model checking to mechanized proving. Today, these verification techniques are challenged by the fact that concurrent software is most likely to be run on multi-core processors equipped with a weak memory semantics (like total store order, TSO), making standard techniques unsound. While for model checking and static analysis techniques, approaches for handling weak memory in verification have already emerged, this is lacking for theorem-prover supported, mechanized correctness proofs.

In this paper, we present the very first approaches to handling TSO semantics in mechanized proofs of linearizability. More precisely, we introduce two approaches, one explicitly modelling store buffers and a second avoiding this modelling by instead reordering program operations. We exemplify and discuss our approach on two case studies, Burns mutual exclusion algorithm and a work stealing dequeue of Arora et al., both of which require additional memory barriers when executed on TSO.

We consider the problem of Partial Quantifier Elimination (PQE). Given formula ∃ X[F(X,Y) ∧ G(X,Y)], where F, G are in conjunctive normal form, the PQE problem is to find a formula F ^*(Y) such that F ^* ∧ ∃ X[G] ≡ ∃ X[F ∧ G]. We solve the PQE problem by generating and adding to F clauses over the free variables that make the clauses of F with quantified variables redundant in ∃ X[F ∧ G]. The traditional Quantifier Elimination problem (QE) can be viewed as a degenerate case of PQE where G is empty so all clauses of the input formula with quantified variables need to be made redundant. The importance of PQE is threefold. First, in non-degenerate cases, PQE can be solved more efficiently than QE. Second, many problems are more naturally formulated in terms of PQE rather than QE. Third, an efficient PQE-algorithm will enable new methods of model checking and SAT-solving. We describe a PQE algorithm based on the machinery of dependency sequents and give experimental results showing the promise of PQE.

Engineering of mission critical software requires a program to be verified that it satisfies a number of properties. This is often done using model checking. However, construction of a program model to be verified and analyzing counterexamples is not an easy task. This can be made easier with the automata-based programming paradigm.

There exist some cases when there are many programs to verify and it is impossible to construct a precise enough finite-state model of the environment. We present an approach for automata program verification under such conditions. Our case study is based on 800 automata programs which solve a simple path-planning problem. As a result, we verified that at least 231 of them are provably correct.

We address the problem of reasoning about interleavings in safety verification of concurrent programs. In the literature, there are two prominent techniques for pruning the search space. First, there are wellinvestigated trace-based methods, collectively known as “Partial Order Reduction (POR)”, which operate by weakening the concept of a trace by abstracting the total order of its transitions into a partial order. Second, there is state-based interpolation where a collection of formulas can be generalized by taking into account the property to be verified. Our main contribution is a framework that synergistically combines POR with state interpolation so that the sum is more than its parts.

Propositional resolution proofs and interpolants derived from them are widely used in automated verification and circuit synthesis. There is a broad consensus that “small is beautiful”—small proofs and interpolants lead to concise abstractions in verification and compact designs in synthesis.Contemporary proof reduction techniques either minimise the proof during construction, or perform a post-hoc transformation of a given resolution proof. We focus on the latter class and present a subsumption-based proof reduction algorithm that extends existing singlepass analyses and relies on a meet-over-all-paths analysis to identify redundant resolution steps and clauses.We show that smaller refutations do not necessarily entail smaller interpolants, and use labelled interpolation systems to generalise our reduction approach to interpolants. Experimental results support the theoretical claims.

This paper aims at improving symbolic model checking for explicit state modeling languages, e.g., Promela, Dve and mCRL2. The modular Pins architecture of LTSmin supports a notion of event locality, by merely indicating for each event on which variables it depends. However, one could distinguish four separate dependencies: read, may-write, must-write and copy. In this paper, we introduce these notions in a language-independent manner. In particular, models with arrays need to distinguish overwriting and copying of values.

We also adapt the symbolic model checking algorithms to exploit the refined dependency information. We have implemented refined dependency matrices for Promela, Dve and mCRL2, in order to compare our new algorithms to the original version of LTSmin. The results show that the amount of successor computations and memory footprint are greatly reduced. Finally, the optimal variable ordering is also affected by the refined dependencies: We determined experimentally that variables with a read dependency should occur at a higher BDD level than variables with a write dependency.

Combinatorial interaction testing (CIT) is an emerging testing technique that has proved to be effective in finding faults due to the interaction among inputs. Efficient test generation for CIT is still an open problem especially when applied to real models having meaningful size and containing many constraints among inputs. In this paper we present a novel technique for the automatic generation of compact test suites starting from models containing constraints given in general form. It is based on the use of Multivalued Decision Diagrams (MDDs) which prove to be suitable to efficiently support CIT. We devise and experiment several optimizations including a novel variation of the classical greedy policy normally used in similar algorithms. The results of a thorough comparison with other similar techniques are presented and show that our approach can provide several advantages in terms of applicability, test suite size, generation time, and cost.

Separation between processes on top of an operating system or between guests in a virtualized environment is essential for establishing security on modern platforms. A key requirement of the underlying hardware is the ability to support multiple partitions executing on the shared hardware without undue interference. For modern processor architectures - with hardware support for memory management, several modes of operation and I/O interfaces - this is a delicate issue requiring deep analysis at both instruction set and processor implementation level. In a first attempt to rigorously answer this type of questions we introduced in previous work an information flow analysis of user program execution on an ARMv7 platform with hardware supported memory protection, but without I/O. The analysis was performed as a semi-automatic proof search procedure on top of an ARMv7 ISA model implemented in the Cambridge HOL4 theorem prover by Fox et al. The restricted platform functionality, however, makes the analysis of limited practical value. In this paper we add support for devices, including DMA, to the analysis. To this end, we propose an approach to device modeling based on the idea of executing devices nondeterministically in parallel with the (single-core) deterministic processor, covering a fine granularity of interactions between the model components. Based on this model and taking the ARMv7 ISA as an example, we provide HOL4 proofs of several noninterference-oriented isolation properties for a partition executing in the presence of devices which potentially use DMA or interrupts.

The IC3 algorithm has proven to be an effective SAT-based safety model checker. It has been generalized to other frameworks such as SMT and applied very successfully to hardware and software model checking. In this paper, we present a novel technique for the supervisory control of discrete-event systems with infinite state space via IC3. We introduce an algorithm for synthesizing maximally permissive controllers using a generalized IC3 to find (if any exists) a weakest inductive invariant predicate which holds in the initial state, is maintained as the system evolves, and implies safety and control properties. To this end, we use a variation of IC3, called Tree-IC3, as a bug finder to solve the supervisory predicate control problem by iteratively reporting all feasible counterexample traces using a tree-like search, while controlling the system to avoid them. The maximally permissiveness is achieved by finding the weakest of such controllers that is invariant under safety and control properties. Experimental results demonstrate the great potential of using IC3 technique for the purpose of the supervisory control problems.

Partial-Order Reduction (POR) is a well-known, successful technique for on-the-fly state space reduction in model checking, as evidenced by the prestigious CAV 2014 award for its pioneers. The combination of POR with LTL model checking is long known to cause the so-called ignoring problem, i.e. relevant behavior is continuously ignored and never selected for exploration. This problem has been solved with increasing sophistication over the years, using various ignoring provisos, which include all necessary actions along cycles in the state space.

However, parallel model checking algorithms still suffer from a lack of an efficient solution; the best known ones causing severe decrease in reductions. We present a new parallel ignoring proviso for POR, which solves this issue by exploiting parallel DFS-based algorithms. Its similarity to the sequential solutions allows the combination with sophisticated earlier methods solving the ignoring problem. We prove correctness of the new proviso and empirically show that it maintains good reductions, runtime performance and parallel scalability.

Constraint solving is a major source of cost in Symbolic Execution (SE). This paper presents a study to assess the importance of some sensible options for solving constraints in SE. The main observation is that stack-based approaches to incremental solving is often much faster compared to cache-based approaches, which are more popular. Considering all 96 C programs from the KLEE benchmark that we analyzed, the median speedup obtained with a (non-optimized) stack-based approach was of 5x. Results suggest that tools should take advantage of incremental solving support from modern SMT solvers and researchers should look for ways to combine stack- and cache-based approaches to reduce execution cost even further. Instructions to reproduce results are available online: http://asa.iti.kit.edu/130_392.php