CAV on Tuesday

Detailed program
Tuesday July 30th, 2002
See also the unified by-slot program

Sessions take place in auditorium 1 unless otherwise indicated.

Session 13: Infinite State Model Checking

Chair: Fabio Somenzi

09:00-09:30  Orna Kupferman, Hebrew U of Jerusalem, Israel
Nir Piterman, Weizmann Inst. of Science, Israel
Moshe Y. Vardi, Rice U, USA
Model checking linear properties of prefix-recognizable systems
We develop an automata-theoretic framework for reasoning about linear properties of 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 automaton that navigates through the tree. For branching properties, the framework is known and the two-way alternating automaton is a tree automaton. Applying the framework for linear properties results in algorithms that are not optimal. Indeed, the fact that a tree automaton can split to copies and simultaneously read all the paths of the tree has a computational price and is irrelevant for linear properties. We introduce path automata on trees. The input to a path automaton is a tree, but the automaton cannot split to copies and it can read only a single path of the tree. In particular, two-way nondeterministic path automata enable exactly the type of navigation that is required in order to check linear properties of infinite-state sequential systems.
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 LTL specifications and prefix-recognizable systems. Our algorithm is exponential in both the size of (the description of) the system and the size of the LTL specification, and we prove a matching lower bound. This is the first optimal algorithm for solving the LTL model-checking problem for prefix recognizable systems. Our framework also handles systems with regular labeling, and in fact we show that LTL model checking with respect to pushdown systems with regular labeling is intereducible with LTL model checking with respect to prefix-recognizable systems with simple labeling.

09:30-10:00  Tatiana Rybina, U Manchester, UK
Andrei Voronkov, U Manchester, UK
Using canonical representations of solutions to speed up infinite-state model checking
In this paper we discuss reachability analysis for infinite-state systems in which states can be represented by a vector of integers. We propose a new algorithm for verifying reachability properties based on canonical representations of solutions instead of decision procedures for integer or real arithmetic. Experimental results demonstrate that problems in protocol verification which are beyond the reach of other existing systems can be solved completely automatically.

10:00-10:30  Walter Hartong, U Hannover, Germany
Lars Hedrich, U Hannover, Germany
Erich Barke, U Hannover, Germany
On discrete modeling and model checking for nonlinear analog systems
In this contribution we present a new method for developing discrete models for nonlinear analog systems. Using an adaptive state space intersection method the main nonlinear properties of the analog system can be retained. Consequently, digital model checking ideas can be applied to analog systems. To describe analog specification properties an extension to the standard model checking language CTL and the appropriate, algorithmic modifications are needed. Two nonlinear examples are given to show the feasibility and the advantages of this method.

Session 14: Compositional Verification II

Chair: Joseph Sifakis

11:00-11:30  Arindam Chakrabarti, U California-Berkeley, USA
Luca de Alfaro, U California-Santa Cruz, USA
Thomas A. Henzinger, U California-Berkeley, USA
Freddy Y. C. Mang, U California-Berkeley, USA
Synchronous and bidirectional component interfaces
Component-based designs are typically conceived using an "optimistic" approach: a component is designed under some assumptions about its environment, with the expectation that the assumptions will be satisfied in the complete design. In turn, the design may describe the behavior of the component only when the component is in an environment that satisfies the assumptions. We present interface models to capture this approach to design. In these models, an interface describes both the input assumptions of a component, and its output behavior. By enabling us to check that the input assumptions of a component are met in a design, interface models provide a basic kind of compatibility check for component-based design. When refining a design into an implementation, interface models require that the implementation behavior of a component satisfies the design specification only when the input assumptions of the component are satisfied, yielding greater flexibility in the choice of implementations.
We present two interface models in detail, one for a simple synchronous form of interaction between components typical in hardware, and the other for more complex synchronous interactions on bidirectional connections. As example for the latter, we specify the interface of a bidirectional bus, with the input assumption that at any time at most one component has write access to the bus. For these interface models, we present algorithms for compatibility and refinement checking, as well as efficient symbolic implementations. We also show how these interface models lead to a rich methodology for the component-based design and analysis of synchronous systems.

11:30-12:00  Arindam Chakrabarti, U California-Berkeley, USA
Luca de Alfaro, U California-Santa Cruz, USA
Thomas A. Henzinger, U California-Berkeley, USA
Marcin Jurdzinski, U California-Berkeley, USA
Freddy Y. C. Mang, U California-Berkeley, USA
Interface compatibility checking for software objects
We present a formal methodology and tool for uncovering errors in the interaction of software objects. Our methodology consists of a suite of languages for defining object interfaces, and algorithms for checking interface compatibility. An object interface makes assumptions about the environment in the form of call and availability constraints. A call constraint restricts the accessibility of local methods to certain external methods. An availability constraint restricts the accessibility of local methods to certain states of the object. For example, an interface for a file server with local methods open and read may assert that a file cannot be read without having been opened. Checking interface compatibility requires the solution of games, and in the case of object interfaces with availability constraints, of pushdown games. Using object interfaces, we have uncovered incompatibilities in TinyOS, a small operating system for sensor nodes in adhoc networks.

12:00-12:30  Michael A. Colón, Stanford U, USA
Henny B. Sipma, Stanford U, USA
Practical methods for proving program termination
We present two algorithms to prove termination of programs by synthesizing linear ranking functions. The first uses an invariant generator based on iterative forward propagation with widening, and extracts ranking functions from the generated invariants by manipulating polyhedral cones. It is capable of finding subtle ranking functions which are linear combinations of many program variables, but is limited to short programs with few variables.
The second, more heuristic, algorithm targets the class of structured programs with single-variable ranking functions. Its invariant generator uses a heuristic extrapolation operator to avoid iterative forward propagation over program loops. For the programs we have considered, this approach converges faster and the invariants it discovers are sufficiently strong to imply the existence of ranking functions.

Session 15: Extended Model Checking

Chair: Gerard J. Holzmann

14:00-14:30  Li Tan, State U of New York-Stony Brook, USA
Rance Cleaveland, State U of New York-Stony Brook, USA
Evidence-based model checking
This paper shows that different "meta-model-checking" analyses can be conducted efficiently on a generic data structure we call a support set. Support sets may be viewed as abstract encodings of the "evidence" a model checker uses to justify the yes/no answers it computes. We indicate how model checkers may be modified to compute supports sets without compromising their time or space complexity. We also show how support sets may be used for a variety of different analyses of model-checking results, including: the generation of diagnostic information for explaining negative model-checking results; and certifying the results of model checking (is the evidence internally consistent?).

14:30-15:00  Gianpiero Cabodi, Polytechnic of Turin, Italy
Sergio Nocco, Polytechnic of Turin, Italy
Stefano Quer, Polytechnic of Turin, Italy
Mixing forward and backward traversals in guided-prioritized BDD-based verification
Over the last decade BDD-based symbolic manipulations have been among the most widely used core technologies in the verification domain and various methodologies have been proposed to improve their efficiency. Following some of the most successful trends proposed in this field, we present in this paper a very promising approach to solve Unbounded Model Checking problems.
Our approach is based on: Mixing forward and backward traversals, dovetailing approximate and exact methods, adopting guided and partitioned searches, efficiently using conjunctive decompositions and generalized cofactor based BDD simplifications. A major contribution of this paper is a backward verification procedure based on a prioritized traversal, that we call "inbound-path-search". The method consists in partitioning state sets in terms of the estimated distance from the "target" set of states, and giving higher priority in the search procedure to the subset with smallest estimated distance. An initial approximate forward traversal produces over-approximated onion-ring frontier sets that are used as distance estimators and guides for prioritized backward traversal. The resulting method is exact and it does not produce any false negatives.
We experimentally compare this methodology with approximate-reachability don't cares in model checking, a state-of-the-art BDD-based technique (implemented in the freely available VIS tool) combining approximate and exact search. We show that we are able to accomplish verification tasks outside its present scope.

15:00-15:30  Mitra Purandare, U Colorado-Boulder, USA
Fabio Somenzi, U Colorado-Boulder, USA
Vacuum cleaning CTL formulae
Vacuity detection in model checking looks for properties that hold in a model, and can be strengthened without causing them to fail. Such properties often signal problems in the model, its environment, or the properties themselves. The seminal paper of Beer et al. proposed an efficient algorithm applicable to a restricted set of properties. Subsequently, Kupferman and Vardi extended vacuity detection to more expressive specification mechanisms. They advocated a more minute examination of temporal logic formulae than the one adopted in [Beer97]. However, they did not address the issues of practicality and usefulness of this more scrupulous inspection. In this paper we discuss efficient algorithms for the detection of vacuous passes of temporal logic formulae, showing that a thorough vacuity check for CTL formulae can be carried out with very small overhead, and even, occasionally, in less time than plain model checking. We also demonstrate the usefulness of such a careful analysis with the help of case studies.

Session 16: Tool Presentations II

Chair: Natarajan Shankar

16:00-16:15  Aaron Stump, Stanford U, USA
Clark W. Barrett, Stanford U, USA
David L. Dill, Stanford U, USA
CVC: a cooperating validity checker
Decision procedures for decidable logics and logical theories have proven to be useful tools in verification. This paper describes the CVC ("a Cooperating Validity Checker") decision procedure. CVC implements a framework for combining subsidiary decision procedures for certain logical theories into a decision procedure for the theories' union. Subsidiary decision procedures for theories of arrays, inductive datatypes, and linear real arithmetic are currently implemented. Other notable features of CVC are the incorporation of the high-performance GRASP solver for propositional reasoning, and the ability to produce independently checkable proofs for valid formulas.

16:15-16:30  Marsha Chechik, U Toronto, Canada
Benet Devereux, U Toronto, Canada
Arie Gurfinkel, U Toronto, Canada
ξChek: A multi-valued model-checker
This paper describes a symbolic multi-valued model-checker XChek.

16:30-16:45  Shoham Ben-David, IBM Haifa, Israel
Anna Gringauze, IBM Haifa, Israel
Baruch Sterin, IBM Haifa, Israel
Yaron Wolfsthal, IBM Haifa, Israel
PathFinder: A tool for design exploration
In this paper we present a tool called PathFinder, which exploits the power of model checking for developing and debugging newly-written hardware designs. Our tool targets the community of design engineers, who-in contrast to verification engineers-are not versed in formal verification, and therefore have traditionally been distant from the growing industry momentum in the area of model checking.
PathFinder provides a means for the designer to explore, debug and gain insight into the behaviors of the design at a very early stage of the implementation-even before their design is complete. In the usage paradigm enabled by PathFinder, which we call Design Exploration, the design engineer specifies a behavior of interest, and the tool then finds and demonstrates-graphically-a set of execution traces compliant with the specified behavior, if any exist. When presented with each such execution sequence, the designer is essentially furnished with an insight into the design behavior, and specifically with an example of a concrete scenario in which the behavior of interest occurs. This scenario can then be closely inspected, refined, or abandoned in favor of another scenario.

16:45-17:00  Dennis Dams, Bell Labs, USA
William Hesse, U Massachusetts, USA
Gerard J. Holzmann, Bell Labs, USA
Abstracting C with abC
A conceptually simple and practically very useful form of data abstraction in model checking is variable hiding, which amounts to suppressing all information about a given set of variables. The abC tool automates this for programs written in the C programming language. It features an integrated demand-driven pointer analysis, and has been implemented as an extension of GCC.

17:00-17:15  Alex Groce, Carnegie Mellon U, USA
Doron A. Peled, U Texas-Austin, USA
Mihalis Yannakakis, Avaya Laboratories, USA
AMC: An adaptive model checker
The AMC (for adaptive model checking) system allows one to perform model checking directly on a system, even when its internal structure is unknown or invisible. It also allows one to perform model checking using an inaccurate model, incrementally improving the model each time that a false negative (i.e., not an actual) counterexample is found.

17:15-18:15  CAV Business Meeting

19:30-22:00  Conference dinner

Room: Restaurant Luftkastellet