Computer Aided Verification

On Friday November 28, 2003, computer scientist and logician Rob Gerth died from sudden cardiac arrest. It is impossible to say all that the loss of Rob means to Intel, to the verification community, and to each of us personally.

This paper reviews the principles behind the paradigm of “abstract interpretation via 3-valued logic,” discusses recent work to extend the approach, and summarizes on-going research aimed at overcoming remaining limitations on the ability to create program-analysis algorithms fully automatically.

We outline a theorem-proving approach to verify pipelined machines. Pipelined machines are complicated to reason about since they involve simultaneous overlapped execution of different instructions. Nevertheless, we show that if the logic used is sufficiently expressive, then it is possible to relate the executions of the pipelined machine with the corresponding Instruction Set Architecture using (stuttering) simulation. Our methodology uses first-order quantification to define a predicate that relates pipeline states with ISA states and uses its Skolem witness for correspondence proofs. Our methodology can be used to reason about generic pipelines with interrupts, stalls, and exceptions, and we demonstrate its use in verifying pipelines mechanically in the ACL2 theorem prover.

On shared memory multiprocessors, synchronization often turns out to be a performance bottleneck and the source of poor fault-tolerance. Lock-free algorithms can do without locking mechanisms, and are therefore desirable. Lock-free algorithms are hard to design correctly, however, even when apparently straightforward. We formalize Herlihy’s methodology [13] for transferring a sequential implementation of any data structure into a lock-free synchronization by means of synchronization primitives Load-linked (LL)/store-conditional (SC). This is done by means of a reduction theorem that enables us to reason about the general lock-free algorithm to be designed on a higher level than the synchronization primitives. The reduction theorem is based on refinement mapping as described by Lamport [10] and has been verified with the higher-order interactive theorem prover PVS. Using the reduction theorem, fewer invariants are required and some invariants are easier to discover and easier to formulate.The lock-free implementation works quite well for small objects. However, for large objects, the approach is not very attractive as the burden of copying the data can be very heavy. We propose two enhanced lock-free algorithms for large objects in which slower processes don’t need to copy the entire object again if their attempts fail. This results in lower copying overhead than in Herlihy’s proposal.

Model checking algorithms can report a property as being true for reasons that may be considered vacuous. Current algorithms for detecting vacuity require either checking a quadratic size witness formula, or multiple model checking runs; either alternative may be quite expensive in practice. Vacuity is, in its essence, a problem with the justification used by the model checker for deeming the property to be true. We argue that current definitions of vacuity are too broad from this perspective and give a new, narrower, formulation. The new formulation leads to a simple detection method that examines only the justification extracted from the model checker in the form of an automatically generated proof. This check requires a small amount of computation after a single verification run on the property, so it is significantly more efficient than the earlier methods. While the new formulation is stronger, and so reports vacuity less often, we show that it agrees with the current formulations for linear temporal properties expressed as automata. Differences arise with inherently branching properties but in instances where the vacuity reported with current formulations is debatable.

We show that termination of a class of linear loop programs is decidable. Linear loop programs are discrete-time linear systems with a loop condition governing termination, that is, a while loop with linear assignments. We relate the termination of such a simple loop, on all initial values, to the eigenvectors corresponding to only the positive real eigenvalues of the matrix defining the loop assignments. This characterization of termination is reminiscent of the famous stability theorems in control theory that characterize stability in terms of eigenvalues.

This paper presents a symbolic model checking algorithm for Fixpoint Logic with Chop, an extension of the modal μ-calculus capable of defining non-regular properties. Some empirical data about running times of a naive implementation of this algorithm are given as well.

Bounded Model Checking, although complete in theory, has been thus far limited in practice to falsification of properties that were not invariants. In this paper we propose a termination criterion for all of LTL, and we show its effectiveness through experiments. Our approach is based on converting the LTL formula to a Büchi automaton so as to reduce model checking to the verification of a fairness constraint. This reduction leads to one termination criterion that applies to all formulae. We also discuss cases for which a dedicated termination test improves bounded model checking efficiency.

We present an unfolding-based approach to LTL-X model-checking of high-level Petri nets. It is based on the method proposed by Esparza and Heljanko for low-level nets [4,5] and a state of the art parallel high-level net unfolder described in [15,13]. We present experimental results comparing our approach to the one of [4,5] and the model-checker Spin [12].

We present a practical compositional interface refinement methodology which helps to integrate formal verification with the design process. One of the main verification challenges is to keep up with the changes to the specifications as the design evolves, and in particular, the transformations to the interfaces between the components. Interface changes are usually incremental, and therefore, the verification efforts after each change should also be incremental in order to be scalable. This paper presents a compositional interface refinement methodology which addresses all of these issues.We have applied this methodology in the design process of a network controller that will be used in the Smart Memory project at Stanford. The design is split into modules which are modeled as transition systems, and the properties of their interfaces are described in the First-Order LTL. We perform interface refinement by compositional reasoning with the help of an additional interface converter module. Unlike in previous approaches, the inverse converter does not need to be constructed, thus, making the verification of the refinement step simpler.

Predicate abstraction has been proved effective for verifying several infinite-state systems. In predicate abstraction, an abstract system is automatically constructed given a set of predicates. Predicate abstraction coupled with automatic predicate discovery provides for a completely automatic verification scheme. For systems with unbounded integer state variables (e.g. software), counterexample guided predicate discovery has been successful in identifying the necessary predicates.For verifying systems with function state variables, which include systems with unbounded memories (microprocessors), arrays in programs, and parameterized systems, an extension to predicate abstraction has been suggested which uses predicates with free (index) variables. Unfortunately, counterexample guidedpredicate discovery is not applicable to this method. In this paper, we propose a simple heuristic for discovering indexed predicates. We illustrate the effectiveness of the approach for verifying safety properties of two systems: (i) a version of the Bakery mutual exclusion protocol, and (ii) a directory-based cache coherence protocol with unbounded FIFO channels per client.

Separation Logic consists of a Boolean combination of predicates of the form v _i ≥ v _j + c where c is a constant and v _i ,v _j are variables of some ordered infinite type like real or integer. Any equality or inequality can be expressed in this logic. We propose a decision procedure for Separation Logic based on allocating small domains (ranges) to the formula’s variables that are sufficient for preserving satisfiability. Given a Separation Logic formula φ, our procedure constructs the inequalities graph of φ, based on φ’s predicates. This graph represents an abstraction of the formula, as there are many formulas with the same set of predicates. Our procedure then analyzes this graph and allocates a range to each variable that is adequate for all of these formulas. This approach of finding small finite ranges and enumerating them symbolically is both theoretically and empirically more efficient than methods based on case-splitting or reduction to Propositional Logic. Experimental results show that the state-space (that is, the number of assignments that need to be enumerated) allocated by our procedure is frequently exponentially smaller than previous methods.

There is a large variety of algorithms for ground decision procedures, but their differences, in particular in terms of experimental performance, are not well studied. We compare the behavior of ground decision procedures by comparing the performance of a variety of technologies on benchmark suites with differing characteristics. Based on these experimental results, we discuss relative strengths and shortcomings of different systems.

The logic of equality with uninterpreted functions (EUF) and its extensions have been widely applied to processor verification, by means of a large variety of progressively more sophisticated (lazy or eager) translations into propositional SAT. Here we propose a new approach, namely a general DPLL(X) engine, whose parameter X can be instantiated with a specialized solver Solver _T for a given theory T, thus producing a system DPLL(T). We describe this DPLL(T) scheme, the interface between DPLL(X) and Solver _T , the architecture of DPLL(X), and our solver for EUF, which includes incremental and backtrackable congruence closure algorithms for dealing with the built-in equality and the integer successor and predecessor symbols. Experiments with a first implementation indicate that our technique already outperforms the previous methods on most benchmarks, and scales up very well.

In this work we focus on model checking of probabilistic models. Probabilistic models are widely used to describe randomized protocols. A Markov chain induces a probability measure on sets of computations. The notion of correctness now becomes probabilistic. We solve here the general problem of linear-time probabilistic model checking with respect to ω-regular specifications. As specification formalism, we use alternating Büchi infinite-word automata, which have emerged recently as a generic specification formalism for developing model checking algorithms. Thus, the problem we solve is: given a Markov chain ${\cal {M}}$ and automaton ${\cal {A}}$, check whether the probability induced by ${\cal {M}}$ of $L({\cal {A}})$ is one (or compute the probability precisely). We show that these problem can be solved within the same complexity bounds as model checking of Markov chains with respect to LTL formulas. Thus, the additional expressive power comes at no penalty.

We propose a new statistical approach to analyzing stochastic systems against specifications given in a sublogic of continuous stochastic logic (CSL). Unlike past numerical and statistical analysis methods, we assume that the system under investigation is an unknown, deployed black-box that can be passively observed to obtain sample traces, but cannot be controlled. Given a set of executions (obtained by Monte Carlo simulation) and a property, our algorithm checks, based on statistical hypothesis testing, whether the sample provides evidence to conclude the satisfaction or violation of a property, and computes a quantitative measure (p-value of the tests) of confidence in its answer; if the sample does not provide statistical evidence to conclude the satisfaction or violation of the property, the algorithm may respond with a “don’t know” answer. We implemented our algorithm in a Java-based prototype tool called VeStA, and experimented with the tool using case studies analyzed in [15]. Our empirical results show that our approach may, at least in some cases, be faster than previous analysis methods.

We propose a compositional specification and verification approach based on GSTE (Generalized Symbolic Trajectory Evaluation). There are two main contributions. First, we propose a specification language that allows concurrent properties be described succinctly in a compositional algebraic manner. Second, we show a precise model checking solution for a compositional specification through automata construction, but much more importantly and practically, we develop an efficient model checking algorithm for directly verifying the compositional specification. At the end, we show the result of our approach in the verification of a micro-instruction scheduler in a state-of-the-art microprocessor.

Verifying whether an ω-regular property is satisfied by a finite-state system is a core problem in model checking. Standard techniques build an automaton with the complementary language, compute its product with the system, and then check for emptiness. Generalized symbolic trajectory evaluation (GSTE) has been recently proposed as an alternative approach, extending the computationally efficient symbolic trajectory evaluation (STE) to general ω-regular properties. In this paper, we show that the GSTE algorithms are essentially a partitioned version of standard symbolic model-checking (SMC) algorithms, where the partitioning is driven by the property under verification. We export this technique of property-driven partitioning to SMC and show that it typically does speed up SMC algorithms.

We present a novel refinement relation (stuck-free conformance) for CCS processes, which satisfies the substitutability property: If I conforms to S, and P is any environment such that P | S is stuck-free, then P | I is stuck-free. Stuck-freedom is related to the CSP notion of deadlock, but it is more discriminative by taking orphan messages in asynchronous systems into account. We prove that conformance is a precongruence on CCS processes, thereby supporting modular refinement. We distinguish conformance from the related preorders, stable failures refinement in CSP and refusal preorder in CCS. We have implemented conformance checking in a new software model checker, zing, and we report on how we used it to find errors in distributed programs.

Boolean Functional Vectors (BFVs) are a symbolic representation for sets of bit-vectors that can be exponentially more compact than the corresponding characteristic functions with BDDs. Additionally, BFVs are the natural representation of bit-vector sets for Symbolic Simulation. Recently, we developed set manipulation algorithms for canonical BFVs by interpreting them as totally ordered selections. In this paper we generalize BFVs by defining them with respect to a partial order. We show that partially ordered BFVs can serve as abstractions for bit-vector sets and can be used to compute over-approximations in reachability analysis. In the special case when the underlying graph of the partial order is a forest, we can efficiently compute an abstract interpretation in a symbolic simulation framework. We present circuit examples where we leverage the exponential gap in the representations and inherent structure in the state-space to demonstrate the usefulness of Partially Ordered Boolean Functional Vectors.

The existence of functional dependency among the state variables of a state transition system was identified as a common cause of inefficient BDD representation in formal verification. Eliminating such dependency from the system compacts the state space and may significantly reduce the verification cost. Despite the importance, how to detect functional dependency without or before knowing the reachable state set remains a challenge. This paper tackles this problem by unifying two closely related, but scattered, studies — detecting signal correspondence and exploiting functional dependency. The prior work on either subject turns out to be a special case of our formulation. Unlike previous approaches, we detect dependency directly from transition functions rather than from reached state sets. Thus, reachability analysis is not a necessity for exploiting dependency. In addition, our procedure can be integrated into reachability analysis as an on-the-fly reduction. Preliminary experiments demonstrate promising results of extracting functional dependency without reachability analysis. Dependencies that were underivable before, due to the limitation of reachability analysis on large transition systems, can now be computed efficiently. For the application to verification, reachability analysis is shown to have substantial reduction in both memory and time consumptions.

This paper shows how to harness decision procedures to automatically verify safety properties of imperative programs that perform dynamic storage allocation and destructive updating of structure fields. Decidable logics that can express reachability properties are used to state properties of linked data structures, while guaranteeing that the verification method always terminates. The main technical contribution is a method of structure simulation in which a set of original structures that we wish to model, e.g., doubly linked lists, nested linked lists, binary trees, etc., are mapped to a set of tractable structures that can be reasoned about using decidable logics. Decidable logics that can express reachability are rather limited in the data structures that they can directly model. For instance, our examples use the logic MSO-E, which can only model function graphs; however, the simulation technique provides an indirect way to model additional data structures.

We introduce a new BDD-like data structure called Hybrid-Restriction Diagrams (HRDs), for the representation and manipulation of linear hybrid automata (LHA) state-spaces, and present algorithms for weakest precondition calculations. This permits us to reason about the valuations of parameters that make safety properties satisfied. Advantages of our approach include the ability to represent discrete state information and concave polyhedra in a unified scheme as well as to save both memory consumptions and manipulation times, when processing the same substructures in state-space representations. Our experimental results document its efficiency in practice.

We present a new abstraction-based framework for deciding satisfiability of quantifier-free Presburger arithmetic formulas. Given a Presburger formula φ, our algorithm invokes a SAT solver to produce proofs of unsatisfiability of approximations of φ. These proofs are in turn used to generate abstractions of φ as inputs to a theorem prover. The SAT-encodings of the approximations of φ are obtained by instantiating the variables of the formula over finite domains. The satisfying integer assignments provided by the theorem prover are then used to selectively increase domain sizes and generate fresh SAT-encodings of φ. The efficiency of this approach derives from the ability of SAT solvers to extract small unsatisfiable cores, leading to small abstracted formulas. We present experimental results which suggest that our algorithm is considerably more efficient than directly invoking the theorem prover on the original formula.

Model checking of infinite state systems is undecidable, therefore, there are instances for which fixpoint computations used in infinite state model checkers do not converge. Given a widening operator one can compute an upper approximation of a least fixpoint in finite number of steps even if the least fixpoint is uncomputable. We present a widening operator for automata encoding integer sets. We show how widening can be used to verify safety properties that cannot be verified otherwise. We also show that the dual of the widening operator can be used to detect counter examples for liveness properties. Finally, we show experimentally how the same technique can be used to verify properties of complex infinite state systems efficiently.

Calculating predictions for an upper bound of the execution time of real-time tasks in embedded systems is a necessary step in designing such systems. There exist successful analysis methods, based on abstract interpretation and integer linear programming (ILP) for that problem. In [12] it is stated, that model checking is not adequate for this task. The approach presented in this paper shows that model checking is adequate and, furthermore, can improve the results. This is done by defining an automaton based semantic for control flow graphs of programs for abstract and concrete instruction cache analysis. A binary search based bunch of model checker runs is used to calculate the upper bound of execution time.

Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems whose states can be represented as words of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of states. We present LTL(MSO), a combination of the logics MSO and LTL as a natural logic for expressing temporal properties to be verified in regular model checking. LTL(MSO) is a two-dimensional modal logic, where MSO is used for specifying properties of system states and transitions, and LTL is used for specifying temporal properties. In addition, the first-order quantification in MSO can be used to express properties parameterized on a position or process. We give a technique for model checking LTL(MSO), which is adapted from the automata-theoretic approach: a formula is translated to a (Büchi) transducer with a regular set of accepting states, and regular model checking techniques are used to search for models. We have implemented the technique and show its application to a number of parameterized algorithms from the literature.

The model checking of a counters system S often reduces to the effective computation of the set of predecessors ${\rm Pre}_S^*(X)$ of a set of integer vectors X. Because the exact computation of this set is not possible in general, we are interested in characterizing the minimal Number Decision Diagrams (NDD) [WB00] that represents the set Pre ≤ k(X). In particular, its size is proved to be just polynomially bounded in k when S is a counters system with a finite monoïd [FL02], explaining why there is no exponential blow up in k.

We propose abstract regular model checking as a new generic technique for verification of parametric and infinite-state systems. The technique combines the two approaches of regular model checking and verification by abstraction. We propose a general framework of the method as well as several concrete ways of abstracting automata or transducers, which we use for modelling systems and encoding sets of their configurations as usual in regular model checking. The abstraction is based on collapsing states of automata (or transducers) and its precision is being incrementally adjusted by analysing spurious counterexamples. We illustrate the technique on verification of a wide range of systems including a novel application of automata-based techniques to an example of systems with dynamic linked data structures.

In this paper we extend the automata-theoretic framework for reasoning about infinite-state sequential systems to handle also the global model-checking problem. 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 a two-way automaton that navigates through the tree. The framework is known for local model checking. For branching time properties, the framework uses two-way alternating automata. For linear time properties, the framework uses two-way path automata. In order to solve the global model-checking problem we show that for both types of automata, given a regular tree, we can construct a nondeterministic word automaton that accepts all the nodes in the tree from which an accepting run of the automaton can start.

We study the problem of formally verifying shared memory multiprocessor executions against memory consistency models—an important step during post-silicon verification of multiprocessor machines. We employ our previously reported style of writing formal specifications for shared memory models in higher order logic (HOL), obtaining intuitive as well as modular specifications. Our specification consists of a conjunction of rules that constrain the global visibility order. Given an execution to be checked, our algorithm generates Boolean constraints that capture the conditions under which the execution is legal under the visibility order. We initially took the approach of specializing the memory model HOL axioms into equivalent (for the execution to be checked) quantified boolean formulae (QBF). As this technique proved inefficient, we took the alternative approach of converting the HOL axioms into a program that generates a SAT instance when run on an execution. In effect, the quantifications in our memory model specification were realized as iterations in the program. The generated Boolean constraints are satisfiable if and only if the given execution is legal under the memory model. We evaluate two different approaches to encode the Boolean constraints, and also incremental techniques to generate and solve Boolean constraints. Key results include a demonstration that we can handle executions of realistic lengths for the modern Intel Itanium memory model. Further research into proper selection of Boolean encodings, incremental SAT checking, efficient handling of transitivity, and the generation of unsatisfiable cores for locating errors are expected to make our technique practical.

In this paper we propose a method for the deductive verification of out-of-order scheduling algorithms. We use tlpvs, our pvs model of linear temporal logic (ltl), to deductively verify the correctness of a model based on the Mips R10000 design. Our proofs use the predicted values method to verify a system including arithmetic and memory operations and speculation. In addition to the abstraction refinement traditionally used to verify safety properties, we also use fairness constraints to prove progress, allowing us to detect errors which may otherwise be overlooked.

Sequential consistency is the archetypal correctness condition for the memory protocols of shared-memory multiprocessors. Typically, such protocols are parameterized by the number of processors, the number of addresses, and the number of distinguishable data values, and typically, automatic protocol verification analyzes only concrete instances of the protocol with small values (generally <3) for the protocol parameters. This paper presents a fully automatic method for proving the sequential consistency of an entire parameterized family of protocols, with the number of processors fixed, but the number of addresses and data values being unbounded parameters. Using some practical, reasonable assumptions (data independence, processor symmetry, location symmetry, simple store ordering, some syntactic restrictions), the method automatically generates a finite-state abstract protocol from the parameterized protocol description; proving sequential consistency of the abstract model, via known methods, guarantees sequential consistency of the entire protocol family. The method is sound, but incomplete, but we argue that it is likely to apply to most real protocols. We present experimental results showing the effectiveness of our method on parameterized versions of the Piranha shared memory protocol and an extended version of a directory protocol from the University of Wisconsin Multifacet Project.

We describe a viable approach for memory abstraction that preserves memory semantics, thereby augmenting the capability of SAT-based BMC to handle designs with large embedded memory without explicitly modeling each memory bit. Our method does not require examining the design or changing the SAT-solver and is guaranteed not to generate false negatives. The proposed method is similar, but with key enhancements, to the previous abstract interpretation of memory that captures its forwarding semantics, i.e., a data read from a memory location is same as the most recent data written at the same location. In our method, we construct an abstract model for BMC by eliminating memory arrays, but retaining the memory interface signals and adding constraints on those signals at every analysis depth to preserve the memory semantics. The size of these memory-modeling constraints depends quadratically on the number of memory accesses and linearly on the bus widths of memory interface signals. Since the analysis depth of BMC bounds the number of memory accesses, these constraints are significantly smaller than the explicit memory model. The novelty of our memory-modeling constraints is that they capture the exclusivity of a read and write pair explicitly, i.e., when a SAT-solver decides on a valid read and write pair, other pairs are implied invalid immediately, thereby reducing the solve time. We have implemented these techniques in our SAT-based BMC framework where we demonstrate the effectiveness of such an abstraction on a number of hardware and software designs with large embedded memories. We show at least an order of magnitude improvement (both in time and space) using our method over explicit modeling of each memory bit. We also show that our method of adding constraints boosts the performance of the SAT solver (in BMC) significantly as opposed to the conventional way of modeling these constraints as nested if-then-else expressions.

The counterexamples produced by model checkers are often lengthy and difficult to understand. In practical verification, showing the existence of a (potential) bug is not enough: the error must be understood, determined to not be a result of faulty specification or assumptions, and, finally, located and corrected. The explain tool uses distance metrics on program executions to provide automated assistance in understanding and localizing errors in ANSI-C programs. explain is integrated with CBMC, a bounded model checker for the C language, and features a GUI front-end that presents error explanations to the user.

Counterexample-driven abstraction refinement is an automatic process that produces abstract models of finite and infinite-state systems. When this process is applied to software, an automatic theorem prover for quantifier-free first-order logic helps to determine the feasibility of program paths and to refine the abstraction. In this paper we report on a fast, lightweight, and automatic theorem prover called Zapato which we have built specifically to solve the queries produced during the abstraction refinement process.

JNuke is a framework for verification and model checking of Java programs. It is a novel combination of run-time verification, explicit-state model checking, and counter-example exploration. Efficiency is crucial in dynamic verification. Therefore JNuke has been written from scratch in C, improving performance and memory usage by an order of magnitude compared to competing approaches and tools.

Our aim is to validate mission-specific components of spacecraft flight software designs that are specified using state-charts and translated automatically to the final flight code for the mission. We established an automatic translation tool set from state-charts to the input language of SPIN for the validation of such mission-specific components. To guarantee compliance with auto-generated flight code, our translation tool set preserves the StateFlow® semantics. We are now able to specify and validate portions of mission-critical software design and implementation using the exhaustive exploration techniques of model checking.

ObsSlice is an optimization tool suited for the verification of timed automata using virtual observers. It discovers the set of modelling elements that can be safely ignored at each location of the observer by synthesizing behavioral dependence information among components. ObsSlice is fed with a network of timed automata and generates a transformed network which is equivalent to the one provided up to branching-time observation. Preliminary results have proven that eliminating irrelevant activity mitigates state space explosion and has a positive -and sometimes dramatic- impact on the performance of verification tools in terms of time, size and counterexample length.

UCLID is a tool for term-level modeling and verification of infinite-state systems expressible in the logic of counter arithmetic with lambda expressions and uninterpreted functions (CLU). In this paper, we describe a key component of the tool, the decision procedure for CLU. Apart from validity checking, the decision procedure also provides other useful features such as concrete counterexample generation and proof-core generation.

The specification formalism employed in model checking is usually some flavour of temporal or process algebraic language that expresses properties of the behavioural aspects of a system. Knowledge [5] is a modality that is orthogonal to the behavioural dimension, capturing properties of information flow. Logics of knowledge have been shown to be a useful framework for the analysis of distributed algorithms and security protocols, and model checking of these logics was first mooted by Halpern and Vardi [6]. Since that time theoretical aspects of model checking the logic of knowledge and its combinations with temporal logic have been studied [8–10]. The system MCK introduced in this paper implements parts of this theory.

The zing project is an effort to build a flexible and scalable model checking infrastructure for concurrent software. The project is divided into four components: (1) a modeling language for expressing concurrent models of software systems, (2) a compiler for translating a zing model into an executable representation of its transition relation, (3) a model checker for exploring the state space of the zing model, and (4) model generators that automatically extract zing models from programs written in common programming languages.

We present in this article the features of the model-checker we have developed: Mec 5. This tool makes it possible to handle models written in the AltaRica language and is characterized by the great expressiveness of its specification logic: μ-calculus on relations with first order quantifiers and equality.

We introduce an integrated tool for implementing and playing various diagnostic games. The tool uses a semantics hierarchy introduced in [6] to improve code sharing among various diagnostic games and reduce the cost of introducing a new game. PlayGame synthesizes the winning strategy using the evidence that is an abstract and uniform encoding of the proof computed by a checker, and hence instead of relying on any particular checker the tool works on a variety of checkers that can be extended to produce such evidence. PlayGame implements a μ-calculus game and a full range of equivalence/preorder games on the Concurrency Workbench-New Century (CWB-NC).

SAL (see http://sal.csl.sri.com) is an open suite of tools for analysis of state machines; it constitutes part of our vision for a Symbolic Analysis Laboratory that will eventually encompass SAL, the PVS verification system, the ICS decision procedures, and other tools developed in our group and elsewhere.SAL provides a language similar to that of PVS, but specialized for the specification of state machines; it was first released with an explicit-state model checker as SAL 1 in July 2002; SAL 2, which was released in December 2003, adds high-performance symbolic and bounded model checkers, and novel infinite bounded and witness model checkers. Both the bounded model checkers can additionally perform verification by k-induction, and the capabilities of all the model checkers and their components are available through an API that is scriptable in Scheme.

JavaFAN is a Java program analysis framework, that can symbolically execute multithreaded programs, detect safety violations searching through an unbounded state space, and verify finite state programs by explicit state model checking. Both Java language and JVM bytecode analyses are possible. JavaFAN’s implementation consists of only 3,000 lines of Maude code, specifying formally the semantics of Java and JVM in rewriting logic and then using the capabilities of Maude for efficient execution, search and LTL model checking of rewriting theories.

We present a toolset for design and verification of Globally Asynchronous Locally Synchronous(GALS) systems. Such systems consist of a network of reactive nodes which have independent clocks and I/O interfaces, and communicate using complex synchronisation mechanisms. GALS systems are gaining prevalence in avionics, embedded systems, and VLSI design. These systems are difficult to design and verify due to the concurrency and complex interaction involved.

This paper presents Web Service Analysis Tool (WSAT), a tool for analyzing and verifying composite web service designs, with the state of the art model checking techniques. Web services are loosely coupled distributed systems communicating via XML messages. Communication among web services is asynchronous, and it is supported by messaging platforms such as JMS which provide FIFO queues to store incoming messages. Data transmission among web services is standardized via XML, and the specification of web service itself (invocation interface and behavior signature) relies on a stack of XML based standards (e.g. WSDL, BPEL4WS, WSCI and etc.). The characteristics of web services, however, raise several challenges in the application of model checking: (1) Numerous competing web service standards, most of which lack formal semantics, complicate the formal specification of web service composition. (2) Asynchronous messaging makes most interesting verification problems undecidable, even when XML message contents are abstracted away [3]. (3) XML data and expressive XPath based manipulation are not supported by current model checkers.

We describe a tool called CVC Lite (CVCL), an automated theorem prover for formulas in a union of first-order theories. CVCL supports a set of theories which are useful in verification, including uninterpreted functions, arrays, records and tuples, and linear arithmetic. New features in CVCL (beyond those provided in similar previous systems) include a library API, more support for producing proofs, some heuristics for reasoning about quantifiers, and support for symbolic simulation primitives.

CirCUs is a satisfiability solver that works on a combination of And-Inverter-Graph, CNF clauses, and BDDs. It has been designed to work well with bounded model checking. It takes as inputs a Boolean circuit (e.g., the model unrolled k times) and an optional set of additional constraints (for instance, requesting that a solution correspond to a simple path) in the form of CNF clauses or BDDs. The algorithms in CirCUs take advantage of the mixed representation by applying powerful BDD-based implication algorithms, and decision heuristics that are objective-driven. CirCUs supports incremental SAT solving, early termination checks, and other analyses of the model that translate into SAT. Experimental results demonstrate CirCUs’s efficiency.

The functional verification of microprocessor designs continues to represent one of the difficult challenges confronting the design of commercial microprocessors. In addition, test logic, transient errors, and power considerations complicate the problems by creating additional complexity and constraints on design solutions. Rigorious mechanized mathematics, often called formal methods, are being used to assist with functional verification and its use has spread to ensuring that test coverage and power limitations are met. While the successes have been notable, the wide-spread use of mathematical methods is still limited. Here we give a brief introduction to formal microprocessor verification, and then we present some scientific and engineering issues that need addressing to bring formal methods into the mainstream.