Automated Technology for Verification and Analysis

Counter-example driven refinement using predicate abstraction has been successfully used to find bugs and verify properties in programs [1]. We describe two recent advances in counter-example driven refinement:

- We present a counter-example driven refinement technique that combines verification and testing [4]. In our approach, we simultaneously use testing and proving, with the goal of either finding a test that demonstrates that

P

violates

ϕ

, or a proof that demonstrates that all executions of

P

satisfy

ϕ

. The most interesting aspect of the approach is that unsuccessful proof attempts are used to generate tests, and unsuccessful attempts to generate tests are used to refine proofs. Besides being theoretically elegant, the approach has practical advantages –precise alias information obtained during tests can be used to greatly aid the efficiency of constructing proofs [5].

- In the past, counter-example driven refinement schemes have worked with a particular form of abstraction called predicate abstraction [1]. We present approaches to refine any abstract interpretation automatically using counterexamples. Several challenges arise: refining using disjunctions leads to powerset domains, and the use of joins forces us to consider counterexample DAGs instead of counterexample traces. We present our solutions to these problems [3,2]. We also present experiences implementing our techniques in a tool

Dagger

.

The essence of formal verification is the modeling, analysis, and, ultimately, understanding of large reactive systems. How do many parts interact to produce appropriate global behavior? How are properties guaranteed over all the possible variations of timing, non-deterministic behavior of components, and a dynamically changing environment?

On the one hand, we would like verification tools to feature powerful automation, but on the other hand, we also want to be able to trust the results with a high degree of confidence. The question of trust in verification tools has been debated for a long time. One popular way of achieving trust in verification tools is through proof generation. However, proof generation could hamstring both the functionality and the efficiency of the automation that can be built into these tools. We argue that trust need not be achieved at the expense of automation, and outline a lightweight approach where the results of untrusted verifiers are checked by a trusted offline checker. The trusted checker is a verified reference kernel that contains a satisfiability solver to support the robust and efficient checking of untrusted tools.

The use of the universal and existential quantifiers with the capability to express the concept of

at least

k

or

all but

k

, for a non-negative integer

k

, has been thoroughly studied in various kinds of logics. In classical logic there are

counting quantifiers

, in modal logics

graded modalities

, in description logics

number restrictions

.

Recently, the complexity issues related to the decidability of the

μ

-calculus, when the universal and existential quantifiers are augmented with graded modalities, have been investigated by Kupfermann, Sattler and Vardi. They have shown that this problem is

ExpTime

-complete.

In this paper we consider another extension of modal logic, the Computational Tree Logic CTL, augmented with graded modalities generalizing standard quantifiers and investigate the complexity issues, with respect to the model-checking problem. We consider a system model represented by a pointed Kripke structure

$\mathcal{K}$

and give an algorithm to solve the model-checking problem running in time

$O(|\mathcal{K}|\cdot |\varphi|)$

which is hence tight for the problem (where |

ϕ

| is the number of temporal and boolean operators and does not include the values occurring in the graded modalities).

In this framework, the graded modalities express the ability to generate a user-defined number of counterexamples (or evidences) to a specification

ϕ

given in

CTL

. However these multiple counterexamples can partially overlap, that is they may share some behavior. We have hence investigated the case when all of them are completely disjoint. In this case we prove that the model-checking problem is both

NP

-hard and

coNP

-hard and give an algorithm for solving it running in polynomial space. We have thus studied a fragment of this graded-

CTL

logic, and have proved that the model-checking problem is solvable in polynomial time.

Recently, genetic programming and model checking were combined for synthesizing algorithms that satisfy a given specification [7,6]. In particular, we demonstrated this approach by developing a tool that was able to rediscover the classical mutual exclusion algorithms [7] with two or three global bits. In this paper we extend the capabilities of the model checking-based genetic programming and the tool built to experiment with this approach. In particular, we add qualitative requirements involving locality of variables and checks, which are typical of realistic mutual exclusion algorithms. The genetic process mimics the actual development of mutual exclusion algorithms, by starting with an existing correct solution, which does not satisfy some performance requirements, and converging into a solution that satisfies these requirements. We demonstrate this by presenting some nontrivial new mutual exclusion algorithms, discovered with our tool.

Model checking has proven to be a useful analysis technique not only for concurrent systems, but also for the genetic regulatory networks (

Grn

s) that govern the functioning of living cells. The applications of model checking in systems biology have revealed that temporal logics should be able to capture both branching-time and fairness properties. At the same time, they should have a user-friendly syntax easy to employ by non-experts. In this paper, we define

Ctrl

(Computation Tree Regular Logic), an extension of

Ctl

with regular expressions and fairness operators that attempts to match these criteria.

Ctrl

subsumes both

Ctl

and

Ltl

, and has a reduced set of temporal operators indexed by regular expressions, inspired from the modalities of

Pdl

(Propositional Dynamic Logic). We also develop a translation of

Ctrl

into

HmlR

(Hennessy-Milner Logic with Recursion), an equational variant of the modal

μ

-calculus. This has allowed us to obtain an on-the-fly model checker with diagnostic for

Ctrl

by directly reusing the verification technology available in the

Cadp

toolbox. We illustrate the application of the

Ctrl

model checker by analyzing the

Grn

controlling the carbon starvation response of

Escherichia coli

.

We present a compositional method for the verification of component-based systems described in a subset of the BIP language encompassing multi-party interaction without data transfer. The method is based on the use of two kinds of invariants. Component invariants which are over-approximations of components’ reachability sets. Interaction invariants which are constraints on the states of components involved in interactions. Interaction invariants are obtained by computing traps of finite-state abstractions of the verified system. The method is applied for deadlock verification in the D-Finder tool. D-Finder is an interactive tool that takes as input BIP programs and applies proof strategies to eliminate potential deadlocks by computing increasingly stronger invariants. The experimental results on non-trivial examples allow either to prove deadlock-freedom or to identify very few deadlock configurations that can be analyzed by using state space exploration.

Multi-valued Model Checking is an extension of classical, two-valued model checking with multi-valued logic. Multi-valuedness has been proved useful in expressing additional information such as incompleteness, uncertainty, and many others, but with the cost of time and space complexity. This paper addresses this problem, and proposes a new algorithm for Multi-valued Model Checking. While Chechik et al. have extended BDD-based Symbolic Model Checking algorithm to the multi-valued case, our algorithm extends Bounded Model Checking (BMC), which can generate a counterexample of minimum length efficiently (if any). A notable feature of our algorithm is that it directly generates conjunctive normal forms, and never reduces multi-valued formulas into many slices of two-valued formulas. To achieve this feature, we extend the BMC algorithm to the multi-valued case and also devise a new translation of multi-valued propositional formulas. Finally, we show experimental results and compare the performance of our algorithm with that of a reduction-based algorithm.

We propose an approach for analyzing non-termination and reachability properties of recursive programs using a combination of over- and under-approximating abstractions. First, we define a new concrete program semantics,

mixed

, that combines both natural and operational semantics, and use it to design an on-the-fly symbolic algorithm. Second, we combine this algorithm with abstraction by following classical fixpoint abstraction techniques. This makes our approach parametrized by different approximating semantics of predicate abstraction and enables a uniform solution for over- and under-approximating semantics. The algorithm is implemented in

Yasm

, and we show that it can establish non-termination of non-trivial C programs completely automatically.

Existing program analysis tools that implement abstraction rely on saturating procedures to compute over-approximations of fixpoints. As an alternative, we propose a new algorithm to compute an over-approximation of the set of reachable states of a program by replacing loops in the control flow graph by their abstract transformer. Our technique is able to generate diagnostic information in case of property violations, which we call

leaping counterexamples

. We have implemented this technique and report experimental results on a set of large ANSI-C programs using abstract domains that focus on properties related to string-buffers.

We present a new property driven pruning algorithm in dynamic model checking to efficiently detect race conditions in multithreaded programs. The main idea is to use a lockset based analysis of observed executions to help prune the search space to be explored by the dynamic search. We assume that a stateless search algorithm is used to systematically execute the program in a depth-first search order. If our conservative lockset analysis shows that a search subspace is race-free, it can be pruned away by avoiding backtracks to certain states in the depth-first search. The new dynamic race detection algorithm is both sound and complete (as precise as the dynamic partial order reduction algorithm by Flanagan and Godefroid). The algorithm is also more efficient in practice, allowing it to scale much better to real-world multithreaded C programs.

Non-freely generated data types are widely used in case studies carried out in the theorem prover KIV. The most common examples are stores, sets and arrays. We present an automatic method that generates finite counterexamples for wrong conjectures and therewith offers a valuable support for proof engineers saving their time otherwise spent on unsuccessful proof attempts. The approach is based on the finite model finding and uses Alloy Analyzer [1] to generate finite instances of theories in KIV [6]. Most definitions of functions or predicates on infinite structures do not preserve the semantics if a transition to arbitrary finite substructures is made. We propose the constraints which should be satisfied by the finite substructures, identify a class of amenable definitions and present a practical realization using Alloy. The technique is evaluated on the library of basic data types as well as on some examples from case studies in KIV.

The linear arithmetic solver in Yices was specifically designed for SMT provers, providing fast support for operations like adding and deleting constraints. We give a procedure for developing interpolants based on the results of the Yices arithmetic solver. For inequalities over real numbers, the interpolant is computed directly from the one contradictory equation and associated bounds. For integer inequalities, a formula is computed from the contradictory equation, the bounds, and the Gomory cuts. The formula is not exactly an interpolant because it may contain local variables. But local variables only arise from Gomory cuts, so there will not be many local variables, and the formula should thereby be useful for applications like predicate abstraction. For integer equalities, we designed a new procedure. It accepts equations and congruence equations, and returns an interpolant. We have implemented our method and give experimental results.

In order to facilitate automated reasoning about large Boolean combinations of non-linear arithmetic constraints involving ordinary differential equations (ODEs), we provide a seamless integration of safe numeric overapproximation of initial-value problems into a SAT-modulo-theory (SMT) approach to interval-based arithmetic constraint solving. Interval-based safe numeric approximation of ODEs is used as an interval contractor being able to narrow candidate sets in phase space in both temporal directions: post-images of ODEs (i.e., sets of states reachable from a set of initial values) are narrowed based on partial information about the initial values and, vice versa, pre-images are narrowed based on partial knowledge about post-sets.

In contrast to the related CLP(F) approach of Hickey and Wittenberg [12], we do (a) support coordinate transformations mitigating the wrapping effect encountered upon iterating interval-based overapproximations of reachable state sets and (b) embed the approach into an SMT framework, thus accelerating the solving process through the algorithmic enhancements of recent SAT solving technology.

We give a method for extending efficient SMT solvers to handle quantifiers, using Superposition inference rules. In our method, the input formula is converted into CNF as in traditional first order logic theorem provers. The ground clauses are given to the SMT solver, which runs a DPLL method to build partial models. The partial model is passed to a Congruence Closure procedure, as is normally done in SMT. Congruence Closure calculates all reduced (dis)equations in the partial model and passes them to a Superposition procedure, along with a justification. The Superposition procedure then performs an inference rule, which we call Justified Superposition, between the (dis)equations and the nonground clauses, plus usual Superposition rules with the nonground clauses. Any resulting ground clauses are provided to the DPLL engine. We prove the completeness of this method, using a nontrivial modification of Bachmair and Ganzinger’s model generation technique. We believe this combination uses the best of both worlds, an SMT process to handle ground clauses efficiently, and a Superposition procedure which uses orderings to handle the nonground clauses.

In the distributed test architecture, a system with multiple ports is tested using a tester at each port/interface, these testers cannot communicate with one another and there is no global clock. Recent work has defined an implementation relation for testing against an input-output transition system in the distributed test architecture. However, this framework placed no restrictions on the test cases and, in particular, allowed them to produce some kind of nondeterminism. In addition, it did not consider the test generation problem. This paper explores the class of controllable test cases for the distributed test architecture, defining a new implementation relation and a test generation algorithm.

Goanna is an industrial-strength static analysis tool used in academia and industry alike to find bugs in C/C++ programs. Unlike existing approaches Goanna uses the off-the-shelf NuSMV model checker as its core analysis engine on a syntactic flow-sensitive program abstraction. The CTL-based model checking approach enables a high degree of flexibility in writing checks, scales to large number of checks, and can scale to large code bases. Moreover, the tool incorporates techniques from constraint solving, classical data flow analysis and a CEGAR inspired counterexample based path reduction. In this paper we describe Goanna’s core technology, its features and the relevant techniques, as well as our experiences of using Goanna on large code bases such as the Firefox web browser.

For quite some time, the Unified Modeling Language (UML) [5] has been adopted by designers of safety critical control systems such as automotive and aviation control. This has led to an increased emphasis on setting up a validation flow over UML that can be used to guarantee the correctness of UML models. In this paper, we present a dynamic property verification (DPV) framework for validation of UML designs. The verification engine is built on top of Rhapsody [3], a popular UML simulator, using the concept of dynamic property monitoring over simulation runs. In view of the growing popularity of model-based development, we believe that the verification methodology presented in this paper is of immediate practical value to the UML-based design community.

As more and more chip design companies attempt to integrate

formal property verification

(FPV) and

assertion-based verification

(ABV) into their pre-silicon validation flows, the main challenge that they face is in the task of expressing the design intent correctly and accurately in terms of formal properties. Incomplete specifications allow bugs to escape detection, while inconsistent specifications lead to the loss of validation effort, since the error lies in the specification itself. In this paper, we present CheckSpec, a tool for automatically checking the consistency and completeness of assertion specifications written in System Verilog Assertions (SVA). CheckSpec comprises of two main engines, namely (a)

Certify

: that certifies a given assertion suite to be free from inconsistencies and (b)

Quantify

: that quantifies the completeness of a given assertion suite. On one hand, CheckSpec will help verification teams to avoid significant waste of validation effort arising out of inconsistent specifications. On the other hand, this will provide a first-cut estimate of the comprehensiveness of an assertion specification suite. The adoption of CheckSpec in the mainstream validation flow can significantly increase the productivity of assertion verification technologies.

We present a tool for parallel shared-memory enumerative LTL model-checking and reachability analysis. The tool is based on distributed-memory algorithms reimplemented specifically for multi-core and multi-cpu environments using shared memory. We show how the parallel algorithms allow the tool to exploit the power of contemporary hardware, which is based on increasing number of CPU cores in a single system, as opposed to increasing speed of a single CPU core.

ALASKA is a verification tool that implements new algorithms based on antichains [5, 7, 6] to efficiently solve the emptiness problem for both alternating finite automata (AFW) and alternating Büchi automata (ABW). Using the well-known translation from LTL to alternating automata, the tool can decide the satisfiability and validity problems for LTL over finite or infinite words. Moreover, ALASKA can solve the model-checking problem for ABW, LTL, AFW and finite-word LTL over symbolic (BDD-encoded) Kripke structures.

NetQi is a freely available model-checker designed to analyze network incidents such as intrusion. This tool is an implementation of the anticipation game framework, a variant of timed game tailored for network analysis. The main purpose of NetQi is to find, given a network initial state and a set of rules, the best strategy that fulfills player objectives by model-checking the anticipation game and comparing the outcome of each play that fulfills strategy constraints. For instance, it can be used to find the best patching strategy. NetQi has been successfully used to analyze service failure due to hardware, network intrusion, worms and multiple-site intrusion defense cooperation.

uppaal

port

is a new tool for component-based design and analysis of embedded systems. It operates on the hierarchically structured continuous time component modeling language SaveCCM and provides efficient model-checking by using partial-order reduction techniques that exploits the structure and the component behavior of the model.

uppaal

port

is implemented as an extension of the verification engine in the

uppaal

tool. The tool can be used as back-end in to the Eclipse based SaveCCM integrated development environment, which supports user friendly editing, simulation, and verification of models.

The evaluation of successor or predecessor state spaces through time progress is a central component in the model-checking algorithm of dense-time automata. The definition of the time progress operator takes into consideration of the path condition of time progress and usually results in high complexity in the evaluation. Previous algorithms in this aspect usually assume that the original location invariance conditions of an automaton are convex in the dense-time state space. Based on this assumption, efficient algorithms for convex path conditions can be designed for reachability analysis. However, it is not clear whether the path conditions are still convex in the general setting of TCTL model-checking. In this work, we discuss the concept of time-convexity that allows us to relax the restrictions on the application of time-progress evaluation algorithm for convex path conditions. Then we give examples in TCTL model-checking that engenders time-concave path conditions even when the original automaton location invariance conditions are time-convex. Then we present two techniques that allow us to apply the evaluation algorithms for time-convex path conditions to time-concave path conditions. Finally, we report our experiment with the techniques. For some benchmarks, our techniques may enhance the performance of model-checking by an order of magnitude.

We identify a new class of decidable hybrid automata: namely, parallel compositions of semi-algebraic o-minimal automata. The class we consider is fundamental to hierarchical modeling in many exemplar systems, both natural and engineered. Unfortunately, parallel composition, which is an atomic operator in such constructions, does not preserve the decidability of reachability. Luckily, this paper is able to show that when one focuses on the composition of semi-algebraic o-minimal automata, it is possible to translate the decidability problem into a satisfiability problem over formulæinvolving both real and integer variables. While in the general case such formulæ would be undecidable, the particular format of the formulæ obtained in our translation allows combining decidability results stemming from both algebraic number theory and first-order logic over (ℝ, 0, 1, + , *, < ) to yield a novel decidability algorithm. From a more general perspective, this paper exposes many new open questions about decidable combinations of real/integer logics.

This paper deals with retrial systems where servers are subject to random vacations. So far, these systems were analyzed only by queueing theory and almost works assumed that the service station consists of one server and the customers source is infinite. In this paper, we give a detailed qualitative and performance analysis of finite-source multiserver retrial systems with multiple and single vacations of servers or all station, using Generalized Stochastic Petri nets. We show how this high level stochastic model allows us to cope with the complexity of such systems involving the simultaneous presence of retrials and vacations, and how stationary performance indices can be expressed as a function of Petri net elements.

We show how fault injection together with recent advances in stochastic model checking can be combined to form a crucial ingredient for improving quantitative safety analysis. Based on standard design notations (Statecharts) annotated with fault occurrence distributions we compute to what extent certain fault configurations contribute to the probability of reaching a safety-critical state.

In order to verify larger and more complicated systems with model checking, it is necessary to apply some abstraction techniques. Using a subset of first-order logic, called EUF, is one of them. The EUF model checking problem is, however, generally undecidable. In this paper, we introduce a technique called term-height reduction, to guarantee the termination of state enumeration in EUF model checking. This technique generates an over-approximate set of states including all the reachable states. By checking a designated invariant property, we can guarantee whether the invariant property always holds for the design, when verification succeeds. We apply our algorithm to a simple C program and a DSP design and show the experimental results.

Classical verification often uses abstraction when dealing with data. On the other hand, dynamic XML-based applications have become pervasive, for instance with the ever growing importance of web services. We define here

Tree Pattern Rewriting Systems

(TPRS) as an abstract model of dynamic XML-based documents. TPRS systems generate infinite transition systems, where states are unranked and unordered trees (hence possibly modeling XML documents). Their guarded transition rules are described by means of tree patterns. Our main result is that given a TPRS system

$(T,{\mathcal R})$

, a tree pattern

P

and some integer

k

such that any reachable document from

T

has depth at most

k

, it is

decidable

(albeit of non elementary complexity) whether some tree matching

P

is reachable from

T

.

We propose a tableau algorithm to decide bisimilarity of guarded normed and unnormed BPA processes, which is very intuitive and direct. It also has the advantage of helping us to show that the equational theory proposed by Hüttel and Stirling for normed BPA systems is also complete for arbitrary guarded BPA systems. As a result, the first equational theory for full BPA processes is found.

We show the solvability of an optimization problem on infinite two-player games. The winning conditions are of the “request-response” format,

i.e.

conjunctions of conditions of the form “if a state with property

Q

is visited, then later a state with property

P

is visited”. We ask for solutions that do not only guarantee the satisfaction of such conditions but also minimal wait times between visits to

Q

-states and subsequent visits to

P

-states. We present a natural class of valuations of infinite plays that captures this optimization problem, and with respect to this measure show the existence of an optimal winning strategy (if a winning strategy exists at all) and that it can be realized by a finite-state machine. For the latter claim we use a reduction to the solution of mean-payoff games due to Paterson and Zwick.

Authentication and secrecy have been widely investigated in security protocols. They are closely related to each other and variants of definitions have been proposed, which focus on the concepts of corresponding assertion and key distribution. This paper proposes an

on-the-fly model checking

method based on the pushdown system to verify the authentication of recursive protocols with an unbounded number of principals. By experiments of the Maude implementation, we find the recursive authentication protocol, which was verified in the sense of (weak) key distribution, has a flaw in the sense of correspondence assertion.

In this paper, a uniform approach for synthesizing monitors checking correctness properties specified in linear-time logics at runtime is provided. Therefore, a generic three-valued semantics is introduced reflecting the idea that

prefixes

of infinite computations are checked. Then a conceptual framework to synthesize monitors from a logical specification to check an execution incrementally is established, with special focus on resorting to the

automata-theoretic approach

. The merits of the presented framework are shown by providing monitor synthesis approaches for a variety of different logics such as

LTL

, the linear-time

μ

-calculus,

PLTL

mod

,

SiS

, and

RLTL

.

Electronic inter-organizational relationships are governed by contracts regulating their interaction, therefore it is necessary to run-time monitor the contracts, as to guarantee their fulfillment. The present work shows how to obtain a run-time monitor for contracts written in

$\mathcal {CL}$

, a formal specification language which allows to write conditional obligations, permissions, and prohibitions over actions. The trace semantics of

$\mathcal {CL}$

formalizes the notion of

a trace fulfills a contract

. We show how to obtain, for a given contract, an alternating Büchi automaton which accepts exactly the traces that fulfill the contract. This automaton is the basis for obtaining a finite state machine which acts as a run-time monitor for

$\mathcal {CL}$

contracts.

This paper shows how the modular structure of composite systems can guide the state-space exploration in explicit-state linear-time model-checking and make it more efficient in practice. Given a composite system where every module has input and output variables — and variables of different modules can be connected — a total ordering according to which variables are generated is determined, through heuristics based on graph-theoretical analysis of the modular structure. The technique is shown to outperform standard exploration techniques (that do not take the modular structure information into account) by several orders of magnitude in experiments with Spin models of MTL formulas.

This paper presents a methodology to perform passive testing based on invariants for systems that present temporal restrictions. Invariants represent the most relevant expected properties of the implementation under test. Intuitively, an invariant expresses the fact that each time the implementation under test performs a given sequence of actions, then it must exhibit a behavior in a lapse of time reflected in the invariant. In particular, the algorithm presented in this paper are fully implemented.