Computer Aided Verification

In this talk, we will consider possible remedies to the State Explosion problem, enabling the verification of large designs. All of these require some user interaction and cannot be done in a fully automatic manner. We will explore the tradeoffs and connections between the different approaches, such as deduction and abstraction, searching for the most natural and convenient mode of user interaction, and speculate about useful additional measures of automation which can make the task of user supervision even simpler.

Protocols using encryption to communicate securely and privately are essential to the protection of our infrastructure. However, since they must be designed to work even under the most hostile conditions, it is not easy to design them correctly. As a matter of fact, it is possible for such protocols to be incorrect even if the cryptographic algorithms they use work perfectly. Thus, over the last few years there has been considerable interest in applying formal methods to the problem of verifying that these protocols are correct. In this talk we give a brief history of this area, and describe some of the emerging issues and new research problems.

Boolean Satisfiability (SAT) is often used as the underlying model for a significant and increasing number of applications in Electronic Design Automation (EDA) as well as in many other fields of Computer Science and Engineering. In recent years, new and efficient algorithms for SAT have been developed, allowing much larger problem instances to be solved. SAT ”packages” are currently expected to have an impact on EDA applications similar to that of BDD packages since their introduction more than a decade ago. This tutorial paper is aimed at introducing the EDA professional to the Boolean satisfiability problem. Specifically, we highlight the use of SAT models to formulate a number of EDA problems in such diverse areas as test pattern generation, circuit delay computation, logic optimization, combinational equivalence checking, bounded model checking and functional test vector generation, among others. In addition, we provide an overview of the algorithmic techniques commonly used for solving SAT, including those that have seen widespread use in specific EDA applications. We categorize these algorithmic techniques, indicating which have been shown to be best suited for which tasks.

Over the last few years there has been an increasing research effort directed towards the automatic verification of infinite-state systems. There are now verification techniques for many classes of infinite-state systems, including timed and hybrid automata, petri nets, pushdown systems, systems with FIFO channels, systems with a simple treatment of data, etc. In this tutorial, we will cover general verification techniques that have been used for infinite-state and parameterized systems, and try to show their power and limitations. Such techniques are e.g., symbolic model-checking techniques, abstraction, induction over the networks structure, widening, and automata-based techniques. We will focus on linear-time safety and liveness properties.

A c-slow netlist N is one which may be retimed to another netlist N ’, where the number of latches along each wire of N ’ is a multiple of c. Leiserson and Saxe [1, page 54] have shown that by increasing c (a process termed slowdown) and retiming, any design may be made systolic, thereby dramatically decreasing its cycle time. In this paper we develop a new fully-automated abstraction algorithm applicable to the verification of generalized c-slow flip-flop based netlists; the more generalized topology accepted by our approach allows applicability to a fairly large class of pipelined netlists. This abstraction reduces the number of state variables and divides the diameter of the model by c; intuitively, it folds the state space of the design modulo c. We study the reachable state space of both the original and reduced netlists, and establish a c-slow bisimulation relation between the two. We demonstrate how CTL* model checking may be preserved through the abstraction for a useful fragment of CTL* formulae. Experiments with two components of IBM’s Gigahertz Processor demonstrate the effectiveness of this abstraction algorithm.

This paper presents a scalable method for parallel symbolic reachability analysis on a distributed-memory environment of workstations. Our method makes use of an adaptive partitioning algorithm which achieves high reduction of space requirements. The memory balance is maintained by dynamically repartitioning the state space throughout the computation. A compact BDD representation allows coordination by shipping BDDs from one machine to another, where different variable orders are allowed. The algorithm uses a distributed termination protocol with none of the memory modules preserving a complete image of the set of reachable states. No external storage is used on the disk; rather, we make use of the network which is much faster.We implemented our method on a standard, loosely-connected environment of workstations, using a high-performance model checker. Our initial performance evaluation using several large circuits shows that our method can handle models that are too large to fit in the memory of a single node. The efficiency of the partitioning algorithm is linear in the number of workstations employed, with a 40-60% efficiency. A corresponding decrease of space requirements is measured throughout the reachability analysis. Our results show that the relatively-slow network does not become a bottleneck, and that computation time is kept reasonably small.

We develop an automata-theoretic framework for reasoning about infinite-state sequential systems. Our framework is based on the observation that states of such systems, which carry a finite but unbounded amount of information, can be viewed as nodes in an infinite tree, and transitions between states can be simulated by finite-state automata. Checking that the system satisfies a temporal property can then be done by an alternating two-way tree automaton that navigates through the tree. As has been the case with finite-state systems, the automata-theoretic framework is quite versatile. We demonstrate it by solving several versions of the model-checking problem for μ-calculus specifications and prefix-recognizable systems, and by solving the realizability and synthesis problems for μ-calculus specifications with respect to prefix-recognizable environments.

We propose a new method for the verification of parameterized cache coherence protocols. Cache coherence protocols are used to maintain data consistency in multiprocessor systems equipped with local fast caches. In our approach we use arithmetic constraints to model possibly infinite sets of global states of a multiprocessor system with many identical caches. In preliminary experiments using symbolic model checkers for infinite-state systems based on real arithmetics (HyTech [HHW97] and DMC [DP99])) we have automatically verified safety properties for parameterized versions of widely implemented write-invalidate and write-update cache coherence policies like the Mesi, Berkeley, Illinois, Firefly and Dragon protocols [Han93]. With this application, we show that symbolic model checking tools originally designed for hybrid and concurrent systems can be applied successfully to a new class of infinite-state systems of practical interest.

We introduce discrete pushdown timed automata that are timed automata with integer-valued clocks augmented with a pushdown stack. A configuration of a discrete pushdown timed automaton includes a control state, finitely many clock values and a stack word. Using a pure automata-theoretic approach, we show that the binary reachability (i.e., the set of all pairs of configurations (α,β), encoded as strings, such that α can reach β through 0 or more transitions) can be accepted by a nondeterministic pushdown machine augmented with reversal-bounded counters (NPCM). Since discrete timed automata with integer-valued clocks can be treated as discrete pushdown timed automata without the pushdown stack, we can show that the binary reachability of a discrete timed automaton can be accepted by a nondeterministic reversal-bounded multicounter machine. Thus, the binary reachability is Presburger. By using the known fact that the emptiness problem is decidable for reversal-bounded NPCMs, the results can be used to verify a number of properties that can not be expressed by timed temporal logics for discrete timed automata and CTL* for pushdown systems.

We consider a variant of the Boolean satisfiability problem where a subset $\cal E$ of the propositional variables appearing in formula F_sat encode a symmetric, transitive, binary relation over N elements. Each of these relational variables, e _i,j , for 1 ≤i < j ≤N, expresses whether or not the relation holds between elements i and j. The task is to either find a satisfying assignment to F_sat that also satisfies all transitivity constraints over the relational variables (e.g., $e_{1,2} \land e_{2,3} \Rightarrow e_{1,3}$), or to prove that no such assignment exists. Solving this satisfiability problem is the final and most difficult step in our decision procedure for a logic of equality with uninterpreted functions. This procedure forms the core of our tool for verifying pipelined microprocessors.To use a conventional Boolean satisfiability checker, we augment the set of clauses expressing F_sat with clauses expressing the transitivity constraints. We consider methods to reduce the number of such clauses based on the sparse structure of the relational variables.To use Ordered Binary Decision Diagrams (OBDDs), we show that for some sets $\cal E$, the OBDD representation of the transitivity constraints has exponential size for all possible variable orderings. By considering only those relational variables that occur in the OBDD representation of F_sat, our experiments show that we can readily construct an OBDD representation of the relevant transitivity constraints and thus solve the constrained satisfiability problem.

The monadic logics M2L-Str and WS1S have been successfully used for verification, although they are nonelementary decidable. Motivated by ideas from bounded model checking, we investigate procedures for bounded model construction for these logics. The problem is, given a formula φ and a bound k, does there exist a word model for φ of length k. We give a bounded model construction algorithm for M2L-Str that runs in a time exponential in k. For WS1S, we prove a negative result: bounded model construction is as hard as validity checking, i.e., it is nonelementary. From this, negative results for other monadic logics, such as S1S, follow. We present too preliminary tests using a SAT-based implementation of bounded model construction; for certain problem classes it can find counter-examples substantially faster than automata-based decision procedures.

Given a Free BDD for the characteristic function of an input-output relation T(x, y), we show how to construct a combinational logic circuit satisfying that relation. Such relations occur as environmental constraints for module specifications, as parts of a proof strategies, or can be computed from existing circuits, e.g., by formal analysis of combinational cycles. The resulting circuit C can be used for further analysis, e.g. symbolic simulation, or to reformat a circuit as a logic optimization tactic.The constructed circuit includes supplementary parametric inputs to allow all legal outputs to be generated in the case that T is non-deterministic. The structure of the circuit is isomorphic to that of the BDD for T, and hence is as compact as the BDD. In particular, when T represents a relation between bit vector integer values definable in Presburger arithmetic, the constructed circuit will have a regular bit slice form.

In this paper we show how to do symbolic model checking using Boolean Expression Diagrams (BEDs), a non-canonical representation for Boolean formulas, instead of Binary Decision Diagrams (BDDs), the traditionally used canonical representation. The method is based on standard fixed point algorithms, combined with BDDs and SAT-solvers to perform satisfiability checking. As a result we are able to model check systems for which standard BDD-based methods fail. For example, we model check a liveness property of a 256 bit shift-and-add multiplier and we are able to find a previously undetected bug in the specification of a 16 bit multiplier. As opposed to Bounded Model Checking (BMC) our method is complete in practice.Our technique is based on a quantification procedure that allows us to eliminate quantifiers in Quantified Boolean Formulas (QBF). The basic step of this procedure is the up-one operation for BEDs. In addition we list a number of important optimizations to reduce the number of basic steps. In particular the optimization rule of quantification-by-substitution turned out to be very useful: $\exists x : g \wedge (x \Leftrightarrow f) \equiv g[f/x]$. The rule is used (1) during fixed point iterations, (2) for deciding whether an initial set of states is a subset of another set of states, and finally (3) for iterative squaring.

Several proof rules based on the assume-guarantee paradigm have been proposed for compositional reasoning about concurrent systems. Some of the rules are syntactically circular in nature, in that assumptions and guarantees appear to be circularly dependent. While these rules are sound, we show that several such rules are incomplete, i.e., there are true properties of a composition that cannot be deduced using these rules. We present a new sound and complete circular rule. We also show that circular and non-circular rules are closely related. For the circular rules defined here, proofs with circular rules can be efficiently transformed to proofs with non-circular rules and vice versa.

We present an automatic iterative abstraction-refinement methodology in which the initial abstract model is generated by an automatic analysis of the control structures in the program to be verified. Abstract models may admit erroneous (or “spurious”) counterexamples. We devise new symbolic techniques which analyze such counterexamples and refine the abstract model correspondingly. The refinement algorithm keeps the size of the abstract state space small due to the use of abstraction functions which distinguish many degrees of abstraction for each program variable. We describe an implementation of our methodology in NuSMV. Practical experiments including a large Fujitsu IP core design with about 500 latches and 10000 lines of SMV code confirm the effectiveness of our approach.

We show how alternating automata provide decision procedures for the equivalence of inductively defined Boolean functions that are useful for reasoning about parameterized families of circuits. We use alternating word automata to formalize families of linearly structured circuits and alternating tree automata to formalize families of tree structured circuits. We provide complexity bounds and show how our decision procedures can be implemented using BDDs. In comparison to previous work, our approach is simpler, yields better complexity bounds, and, in the case of tree structured families, is more general.

Any formal method or tool is almost certainly more often applied in situations where the outcome is failure (a counterexample) rather than success (a correctness proof). We present a method for symbolic model checking that can lead to significant time and memory savings for model-checking runs that fail, while occurring only a small overhead for model-checking runs that succeed. Our method discovers an error as soon as it cannot be prevented, which can be long before it actually occurs; for example, the violation of an invariant may become unpreventable many transitions before the invariant is violated.The key observation is that “unpreventability” is a local property of a single module: an error is unpreventable in a module state if no environment can prevent it. Therefore, unpreventability is inexpensive to compute for each module, yet can save much work in the state exploration of the global, compound system. Based on different degrees of information available about the environment, we define and implement several notions of “unpreventability,” including the standard notion of uncontrollability from discrete-event control. We present experimental results for two examples, a distributed database protocol and a wireless communication protocol.

A discrete strategy improvement algorithm is given for constructing winning strategies in parity games, thereby providing also a new solution of the model-checking problem for the modal μ-calculus. Known strategy improvement algorithms, as proposed for stochastic games by Hoffman and Karp in 1966, and for discounted payoff games and parity games by Puri in 1995, work with real numbers and require solving linear programming instances involving high precision arithmetic. In the present algorithm for parity games these difficulties are avoided by the use of discrete vertex valuations in which information about the relevance of vertices and certain distances is coded. An efficient implementation is given for a strategy improvement step. Another advantage of the present approach is that it provides a better conceptual understanding and easier analysis of strategy improvement algorithms for parity games. However, so far it is not known whether the present algorithm works in polynomial time. The long standing problem whether parity games can be solved in polynomial time remains open.

In this paper we address the problem of distributing model checking of timed automata. We demonstrate through four real life examples that the combined processing and memory resources of multi-processor computers can be effectively utilized. The approach assumes a distributed memory model and is applied to both a network of workstations and a symmetric multiprocessor machine. However, certain unexpected phenomena have to be taken into account. We show how in the timed case the search order of the state space is crucial for the effectiveness and scalability of the exploration. An effective heuristic to counter the effect of the search order is provided. Some of the results open up for improvements in the single processor case.

We study model checking problems for pushdown systems and linear time logics. We show that the global model checking problem (computing the set of configurations, reachable or not, that violate the formula) can be solved in $O({g_{\cal P}}{g_{\cal P}}^3{g_{\cal B}}{g_{\cal B}}^3)$ time and $O({g_{\cal P}}{g_{\cal P}}^2{g_{\cal B}}{g_{\cal B}}^2)$ space, where ${g_{\cal P}}{g_{\cal P}}$ and ${g_{\cal B}}{g_{\cal B}}$ are the size of the pushdown system and the size of a Büchi automaton for the negation of the formula. The global model checking problem for reachable configurations can be solved in $O({g_{\cal P}}{g_{\cal P}}^4{g_{\cal B}}{g_{\cal B}}^3)$ time and $O({g_{\cal P}}{g_{\cal P}}^4{g_{\cal B}}{g_{\cal B}}^2)$ space. In the case of pushdown systems with constant number of control states (relevant for our application), the complexity becomes $O({g_{\cal P}}{g_{\cal P}}{g_{\cal B}}{g_{\cal B}}^3)$ time and $O({g_{\cal P}}{g_{\cal P}}{g_{\cal B}}{g_{\cal B}}^2)$ space and $O({g_{\cal P}}{g_{\cal P}}^2{g_{\cal B}}{g_{\cal B}}^3)$ time and $O({g_{\cal P}}{g_{\cal P}}^2{g_{\cal B}}{g_{\cal B}}^2)$ space, respectively. We show applications of these results in the area of program analysis and present some experimental results.

We present an algorithm to generate small Büchi automata for LTL formulae. We describe a heuristic approach consisting of three phases: rewriting of the formula, an optimized translation procedure, and simplification of the resulting automaton. We present a translation procedure that is optimal within a certain class of translation procedures. The simplification algorithm can be used for Büchi automata in general. It reduces the number of states and transitions, as well as the number and size of the accepting sets—possibly reducing the strength of the resulting automaton. This leads to more efficient model checking of linear-time logic formulae. We compare our method to previous work, and show that it is significantly more efficient for both random formulae, and formulae in common use and from the literature.

A new approach is presented for detecting whether a particular computation of an asynchronous distributed system satisfies $\mathop{{\bf Poss}}\Phi$ (read “possibly Φ”), meaning the system could have passed through a global state satisfying predicate Φ, or $\mathop{{\bf Def}}\Phi$ (read “definitely Φ”), meaning the system definitely passed through a global state satisfying Φ. Detection can be done easily by straightforward state-space search; this is essentially what Cooper and Marzullo proposed. We show that the persistent-set technique, a well-known partial-order method for optimizing state-space search, provides efficient detection. This approach achieves the same worst-case asymptotic time complexity as two special-purpose detection algorithms of Garg and Waldecker that detect $\mathop{{\bf Poss}}\Phi$ and $\mathop{{\bf Def}}\Phi$ for a restricted but important class of predicates. For $\mathop{{\bf Poss}}\Phi$, our approach applies to arbitrary predicates and thus is more general than Garg and Waldecker’s algorithm. We apply our algorithm for $\mathop{{\bf Poss}}\Phi$ to two examples, achieving a speedup of over 700 in one example and over 70 in the other, compared to unoptimized state-space search.

Hierarchical state machines is a popular visual formalism for software specifications. To apply automated analysis to such specifications, the traditional approach is to compile them to existing model checkers. Aimed at exploiting the modular structure more effectively, our approach is to develop algorithms that work directly on the hierarchical structure. First, we report on an implementation of a visual hierarchical language with modular features such as nested modes, variable scoping, mode reuse, exceptions, group transitions, and history. Then, we identify a variety of heuristics to exploit these modular features during reachability analysis. We report on an enumerative as well as a symbolic checker, and case studies.

This is a study of the formal verification of a VLIW microprocessor that imitates the Intel Itanium [9][12][17] in features such as predicated execution, register remapping, advanced and speculative loads, and branch prediction. The formal verification is done with the Burch and Dill flushing technique [5] by exploiting the properties of Positive Equality [3][4]. The contributions include an extensive use of conservative approximations in abstracting portions of the processor and a framework for decomposition of the Boolean evaluation of the correctness formula. The conservative approximations are applied automatically when abstracting a memory whose forwarding logic is not affected by stalling conditions that preserve the correctness of the memory semantics for the same memory. These techniques allow a reduction of more than a factor of 4 in the CPU time for the formal verification of the most complex processor model examined relative to the monolithic evaluation of the correctness formula for a version of the same processor where conservative approximations are not applied.

This paper describes a technique of inductive proof based on model checking. It differs from previous techniques that combine induction and model checking in that the proof is fully mechanically checked and temporal variables (process identifiers, for example) may be natural numbers. To prove ∀n.ϕ(n) inductively, the predicate $\varphi(n-1) \Rightarrow \varphi(n)$ must be proved for all values of the parameter n. Its proof for a fixed n uses a conservative abstraction that partitions the natural numbers into a finite number of intervals. This renders the model finite. Further, the abstractions for different values of n fall into a finite number of isomorphism classes. Thus, an inductive proof of ∀n.ϕ(n) can be obtained by checking a finite number of formulas on finite models. The method is integrated with a compositional proof system based on the SMV model checker. It is illustrated by examples, including the N-process “bakery” mutual exclusion algorithm.

The paper considers the problem of uniform verification of parameterizedsystems by symbolic model checking, using formulas in fs1s (a syntactic variant of the 2nd order logic ws1s) for the symbolic representation of sets of states. The technical difficulty addressed in this work is that, in many cases, standard model-checking computations fail to converge.Using the tool tlv [P], we formulated a general approach to the acceleration of the transition relations, allowing an unbounded number of different processes to change their local state (or interact with their neighbor) in a single step. We demonstrate that this acceleration process solves the difficulty and enables an efficient symbolic model-checking of many parameterized systems such as mutual-exclusion and token-passing protocols for any value of N, the parameter specifying the size of the system.Most previous approaches to the uniform verification of parameterized systems, only considered safety properties of such systems. In this paper, we present an approach to the verification of iveness properties and demonstrate its application to prove accessibility properties of the considered protocols.

The Available Bit Rate protocol (ABR) for ATM networks is well-adapted to data traffic by providing minimum rate guarantees and low cell loss to the ABR source end system. An ABR conformance algorithm for controlling the source rates through an interface has been defined by ATM Forum and a more efficient version of it has been designed in [13]. We present in this work the first complete mechanical verification of the equivalence between these two algorithms. The proof is involved and has been supported by the PVS theorem-prover. It has required many lemmas, case analysis and induction reasoning for the manipulation of unbounded scheduling lists. Some ABR conformance protocols have been verified in previous works. However these protocols are approximations of the one we consider here. For instance, the algorithms mechanically proved in [10] and [5] consider scheduling lists with only two elements.

The verification of continuous-time Markov chains (CTMCs) against continuous stochastic logic (CSL) [3,6], a stochastic branching-time temporal logic, is considered. CSL facilitates among others the specification of steady-state properties and the specification of probabilistic timing properties of the form ${\cal P}_{\bowtie p}(\Phi_1 \, {\cal U}^{I} \, \Phi_2)$, for state formulas Φ₁ and Φ₂, comparison operator ⋈, probability p, and real interval I. The main result of this paper is that model checking probabilistic timing properties can be reduced to the problem of computing transient state probabilities for CTMCs. This allows us to verify such properties by using efficient techniques for transient analysis of CTMCs such as uniformisation. A second result is that a variant of ordinary lumping equivalence (i.e., bisimulation), a well-known notion for aggregating CTMCs, preserves the validity of all CSL-formulas.

In this paper we present a semi-algorithm to do compositional model-checking for hybrid systems. We first define a modal logic $L_{\nu}^h$ which is expressively complete for linear hybrid automata. We then show that it is possible to extend the result on compositional model-checking for parallel compositions of finite automata and networks of timed automata to linear hybrid automata. Finally we present some results obtained with an extension of the tool CMC to handle a subclass of hybrid automata (the stopwatch automata).

Our experience with semi-exhaustive verification shows a severe degradation in usability for the corner-case bugs, where the tuning effort becomes much higher and recovery from dead-ends is more and more difficult. Moreover, when there are no bugs at all, shifting semi-exhaustive traversal to exhaustive traversal is very expensive, if not impossible. This makes the output of semi-exhaustive verification on non-buggy designs very ambiguous. Furthermore, since after the design fixes each falsification task needs to converge to full verification, there is a strong need for an algorithm that can handle efficiently both verification and falsification. We address these shortcomings with an enhanced reachability algorithm that is more robust in detecting corner-case bugs and that can potentially converge to exhaustive reachability. Our approach is similar to that of Cabodi et al. in partitioning the frontiers during the traversal, but differs in two respects. First, our partitioning algorithm trades quality for time resulting in a significantly faster traversal. Second, the subfrontiers are processed according to some priority function resulting in a mixed BFS/DFS traversal. It is this last feature that makes our algorithm suitable for both falsification and verification.

We present regular model checking, a framework for algorithmic verification of infinite-state systems with, e.g., queues, stacks, integers, or a parameterized linear topology. States are represented by strings over a finite alphabet and the transition relation by a regular length-preserving relation on strings. Major problems in the verification of parameterized and infinite-state systems are to compute the set of states that are reachable from some set of initial states, and to compute the transitive closure of the transition relation. We present two complementary techniques for these problems. One is a direct automata-theoretic construction, and the other is based on widening. Both techniques are incomplete in general, but we give sufficient conditions under which they work. We also present a method for verifying ω-regular properties of parameterized systems, by computation of the transitive closure of a transition relation.

We address the problem of automatic analysis of parametric counter and clock automata. We propose a semi-algorithmic approach based on using (1) expressive symbolic representation structures called Parametric DBM’s, and (2) accurate extrapolation techniques allowing to speed up the reachability analysis and help its termination. The techniques we propose consist in guessing automatically the effect of iterating a control loop an arbitray number of times, and in checking that this guess is exact. Our approach can deal uniformly with systems that generate linear or nonlinear sets of configurations. We have implemented our techniques and experimented them on nontrivial examples such as a parametric timed version of the Bounded Retransmission Protocol.

We present an algorithm that constructs a finite state “abstract” program from a given, possibly infinite state, “concrete” program by means of a syntactic program transformation. Starting with an initial set of predicates from a specification, the algorithm iteratively computes the predicates required for the abstraction relative to that specification. These predicates are represented by boolean variables in the abstract program. We show that the method is sound, in that the abstract program is always guaranteed to simulate the original. We also show that the method is complete, in that, if the concrete program has a finite abstraction with respect to simulation (bisimulation) equivalence, the algorithm can produce a finite simulation-equivalent (bisimulation-equivalent) abstract program. Syntactic abstraction has two key advantages: it can be applied to infinite state programs or programs with large data paths, and it permits the effective application of other reduction methods for model checking. We show that our method generalizes several known algorithms for analyzing syntactically restricted, data-insensitive programs.

This paper introduces temporal-logic queries for model understanding and model checking. A temporal-logic query is a temporal-logic formula in which a placeholder appears exactly once. Given a model, the semantics of a query is a proposition that can replace the placeholder to result in a formula that holds in the model and is as strong as possible. The author defines a class of CTL queries that can be evaluated in linear time, and show how they can be used to help the user understand the system behaviors and obtain more feedback in model checking.

In classical timed automata, as defined by Alur and Dill [AD90,AD94] and since widely studied, the only operation allowed to modify the clocks is the reset operation. For instance, a clock can neither be set to a non-null constant value, nor be set to the value of another clock nor, in a non-deterministic way, to some value lower or higher than a given constant. In this paper we study in details such updates.We characterize in a thin way the frontier between decidability and undecidability. Our main contributions are the following :We exhibit many classes of updates for which emptiness is undecidable. These classes depend on the clock constraints that are used – diagonal-free or not – whereas it is well known that these two kinds of constraints are equivalent for classical timed automata.We propose a generalization of the region automaton proposed by Alur and Dill, allowing to handle larger classes of updates. The complexity of the decision procedure remains Pspace-complete.

Bounded Model Checking based on SAT methods has recently been introduced as a complementary technique to BDD-based Symbolic Model Checking. The basic idea is to search for a counter example in executions whose length is bounded by some integer k. The BMC problem can be efficiently reduced to a propositional satisfiability problem, and can therefore be solved by SAT methods rather than BDDs. SAT procedures are based on general-purpose heuristics that are designed for any propositional formula. We show that the unique characteristics of BMC formulas can be exploited for a variety of optimizations in the SAT checking procedure. Experiments with these optimizations on real designs proved their efficiency in many of the hard test cases, comparing to both the standard SAT procedure and a BDD-based model checker.

Net unfoldings have attracted much attention as a powerful technique for combating state space explosion in model checking. The method has been applied to verification of 1-safe (finite) Petri nets, and more recently also to other classes of finite-state systems such as synchronous products of finite transition systems. We show how unfoldings can be extended to the context of infinite-state systems. More precisely, we apply unfoldings to get an efficient symbolic algorithm for checking safety properties of unbounded Petri nets. We demonstrate the advantages of our method by a number of experimental results.

I describe a systematic method for deductive verification of safety properties of concurrent programs. The method has much in common with the “verification diagrams” of Manna and Pnueli [17], but derives from different intuitions. It is based on the idea of strengthening a putative safety property into a disjunction of “configurations” that can easily be proved to be inductive. Transitions among the configurations have a natural diagrammatic representation that conveys insight into the operation of the program. The method lends itself to mechanization and is illustrated using a simplified version of an example that had defeated previous attempts at deductive verification.

In this paper, we discuss the verification of a microprocessor involving a reorder buffer, a store buffer, speculative execution and exceptions at the microarchitectural level. We extend the earlier proposed Completion Functions Approach [HSG98] in a uniform manner to handle the verification of such microarchitectures. The key extension to our previous work was in systematically extending the abstraction map to accommodate the possibility of all the pending instructions being squashed. An interesting detail that arises in doing so is how the commutativity obligation for the program counter is proved despite the program counter being updated by both the instruction fetch stage (when a speculative branch may be entertained) and the retirement stage (when the speculation may be discovered to be incorrect). Another interesting detail pertains to how store buffers are handled. We highlight a new type of invariant in this work—one which keeps correspondence between store buffer pointers and reorder buffer pointers. All these results, taken together with the features handled using the completion functions approach in our earlier published work [HSG98,HSG99,HGS99], demonstrates that the approach is uniformly applicable to a wide variety of pipelined designs.

For the foreseeable future, industrial hardware design will continue to use both simulation and model checking in the design verification process. To date, these techniques are applied in isolation using different tools and methodologies, and different formulations of the problem. This results in cumulative high cost and little (if any) cross-leverage of the individual advantages of simulation and formal verification.

Formal validation of distributed systems relies on several specification formalisms (such as the international standards LOTOS [15] or SDL [16]), and it requires different kinds of tools to cover the whole development process. Presently, a wide range of tools are available, either commercial or academic ones, but none of them fulfills in itself all the practical needs.

There is a growing trend to integrate theorem proving systems with specialized decision procedures and model checking systems. The proving capabilities of the PVS theorem prover, for example, have been improved considerably by extending it with new proof tactics based on a BDD package, a μ-calculus model-checker [4], and a polyhedral library. In this way, a theorem proving system like PVS provides a common front-end and specification language for a variety of specialized tools. This makes it possible to use a whole arsenal of verification and validation methods in a seamless way, combine them using a strategy language, and provide development chain analysis.

We describe here the Pet (standing for path exploration tool) system, developed in Bell Labs. This new tool allows an interactive testing of sequential or concurrent programs, using techniques taken from deductive program verification. It automatically generates and displays a graphical representation of the flow graph, and links the visual representation to the code. Testing is done by selecting execution paths, or, in the case of concurrent programs, interleaved sequences of code. The Pet system calculates the exact condition to execute path being selected, in terms of the program variables. It also calculates (when possible) whether this condition is vacuous (never satisfied) or universal (always satisfied). The user can then edit the path and select variants of it by either extending it, truncating it, or switching the order of appearance of concurrent events. This testing approach is not limited to finite state systems, and hence can be used in cases where a completely automatic verification cannot be applied.

In earlier work, Necula and Lee developed proof-carrying code (PCC) [3,5],which is a mechanism for ensuring the safe behavior of programs. In PCC, a program contains both the code and an encoding of an easy-to-check proof. The validity of the proof, which can be automatically determined by a simple proof-checking program, implies that the code, when executed, will behave safely according to a user-supplied formal definition of safe behavior. Later, Necula and Lee demonstrated the concept of a certifying compiler [6,7].Certifying compilers promise to make PCC more practical by compiling high-level source programs into optimized PCC binaries completely automatically, as opposed to depending on semi-automatic theorem-proving techniques. Taken together, PCC and certifying compilers provide a possible solution to the code safety problem, even in applications involving mobile code [4].

The Statemate Verification Environment supports requirement analysis and specification development of embedded controllers as part of the Statemate product offering of I-Logix, Inc. This paper discusses key enhancements of the prototype tool reported in [2,5] in order to enable full scale industrial usage of the tool-set. It thus reports on a successfully completed technology transfer from a prototype tool-set to a commercial offering. The discussed enhancements are substantiated with performance results all taken from real industrial applications of leading companies in automotive and avionics.

In recent years, a number of cryptographic protocols have been mechanically verified using a variety of inductive methods (e.g., [4,3,5]).These proofs typically require defining a number of recursive sets of messages, and require deep insight into why the protocol is correct. As a result, these proofs often require days to weeks of expert effort.

Asynchronous circuit design can probably avoid the occurrence of various problems which arise in designing large synchronous circuits, such as clock skews and high power consumption. On the other hand, the cost of the verification of asynchronous circuits is usually much higher than that of synchronous circuits. This is because every change of wires should be taken into account in order to capture the behavior of asynchronous circuits unlike in the case of synchronous circuits. Furthermore, asynchronous circuit designers have recently preferred to use timed circuits for implementing fast and compact circuits. This trend increases the cost of verification, and at the same time increases the demands for formal verification tools. VINAS-P is our newest formal verification tool for timed asynchronous circuits using the techniques proposed in [1].The main idea in these techniques is the partial order reduction based on the timed version [2] of the Stubborn set method [3].

XMC is a toolset for specifying and verifying concurrent systems. Its main mode of verification is temporal-logic model checking [CES86], although equivalence checkers have also been implemented. In its current form, temporal properties are specified in the alternation-free fragment of the modal mu-calculus [Koz83], and system models are specified in XL, a value-passing language based on CCS [Mil89]. The core computational components of the XMC system, such as those for compiling the specification language, model checking, etc., are built on top of the XSB tabled logic-programming system [XSB99].