DIMACS Series in
Discrete Mathematics and Theoretical Computer Science

EDITORS: E.M. Clarke and R.P. Kurshan
Published by the American Mathematical Society

Ordering Information

This volume may be obtained from the AMS or through bookstores in your area.

To order through AMS contact the AMS Customer Services Department, P.O. Box 6248, Providence, Rhode Island 02940-6248 USA. For Visa, Mastercard, Discover, and American Express orders call 1-800-321-4AMS.

You may also visit the AMS Bookstore and order directly from there. DIMACS does not distribute or sell these books.


This volume is devoted to the proceedings of the second workshop on "Computer-Aided Verification" (the first to use this specific title). The motivation for a specific workshop in computer-aided verification (CAV) is to bring together researchers working on effective algorithms or methodologies for formal verification (as distinguished, say, from attributes of logics or formal languages). The considerable interest generated by the first workshop (held in Grenoble, June 1989) motivates this meeting. As this interest continued to grow, it was decided to continue CAV on an annual basis, and for that purpose the CAV Steering Committee was formed (see below). In view of this, we take the opportunity here to state the focus of CAV and briefly sketch the history of research in formal verification as it relates to CAV.

It is the intention of the CAV Steering Committee that future CAV meetings will continue the current focus on the problem of making formal verification feasible for various models of computation. Present emphasis is on models associated with distributed programs, protocols, and digital circuits. A good test of algorithm feasibility is to embed it into a verification tool and exercise that tool on realistic examples. Thus, we have promoted special sessions for the demonstration of new verification tools. For the technical sessions, we seek theoretical results that lead to new or more powerful verification methods. We expect that there will be less emphasis at CAV meetings on purely theoretical results in program logics--not because fundamental results of this type are unimportant but because this research is adequately covered in other conferences. Since we expect that a number of the results presented at CAV actually will be used by hardware and software designers, we seek to maintain a balance between presentations by researchers and practitioners.

Proofs of correctness of algorithms such as the Euclidean algorithm go far back into history. The importance of such proofs in computing apparently was realized by Turing. However, it was not until the 1960s and early 1970s that provably correct computation began to attract much attention as a self-contained area of research. Fundamental contributions in this period established the vehicles through which formal proofs of program correctness could be constructed from axioms and rules of inference in the same way that proofs in mathematics are constructed.

The first proofs of programs were hand constructed and, therefore, quite short and easy to follow. As a general approach, however, manually constructed proofs of correctness were beset by two fundamental problems. First was the problem of scalability: real programs tend to be long and intricate (compared with the statement of a mathematical theorem), so a proof of correctness could be expected to be correspondingly long. Under these circumstances, it was unclear to what extent a methodology based upon manually constructed proofs could be expected to be successful. The second problem was credibility: unlike published mathematics which may be expected to undergo extensive peer review, proofs of programs are more likely to be read only by the author.

Much interesting work has continued in this direction, however, and through the middle 1980s, most of the weight of research on formal verification (as this area of research became known) remained focused upon manual proofs of correctness. Applications of the work mainly did not overcome these two fundamental problems.

The purpose of CAV is to feature research specifically directed at overcoming these two problems of scalability and credibility. Presently, this thrust has become synonymous with computer-aided verification.

Initially, researchers thought that computer programs for theorem-proving could be used in automatic program verification. Logics emerged as a mechanism to formalize the manipulation of the properties to be proved. Out of fundamental work in logic and mathematics, automatic theorem-proving advanced rapidly. Automated theorem-proving had its own problems, however, stemming largely from its nonalgorithmic nature and basic problems of tractability and decidability. These difficulties seemed to provide obstacles which were much too difficult for early theorem-provers to overcome. Many of the pioneers in program verification became disillusioned and moved into other research areas where progress was more rapid.

Recent advances and the maturation of theorem-provers (and more specifically, proof-checkers) has renewed interest in their application to practical tasks such as hardware verification. Currently, this direction has demonstrated applicability for proving properties of data paths in hardware designs. Theorem-proving has been less successful in verifying properties related to control, particularly when concurrency and process synchronization are involved.

Together with the early disillusionment in theorem-provers emerged an intense interest in restricted logics for which formula satisfiability, used to test f=> g, is decidable. Preeminent among these logics was temporal logic.

However, this work had two significant deficiencies of its own. First, these logics invariably constituted a substantial abstraction of a restricted class of programs. In fact, abstraction was so great that formulas in the logic lost their connection to the programs they were meant to abstract. Second, as a purely computational matter, decision procedures still were largely intractable, being exponential in the size of the formulas.

This second problem was undercut in 1980 through the introduction of model-checking as an alternative to checking formula satisfiability. Not only was linear-time model-checking demonstrated (for branching-time temporal logic), but perhaps the first computer implementations of practical formal verification algorithms were produced, as well. Computational complexity nonetheless remained an issue: while model-checking could be done in time linear in the size of the model, the model itself grows exponentially in the number of model components; for "real" models, complexity still was the gating issue.

This problem and the problem of bridging the gap from model to implementation were addressed soon after through the introduction of homomorphic reduction. This permitted checking complex models indirectly through checks on reductions which are relative to the respective properties under test. Homomorphism also served as a mechanism for stepwise refinement, relating implementations to design models. This led to compositional and hierarchical verification, as well as specialized reduction methods involving certain types of induction. Complexity still remained an issue, however, as homomorphic reductions may be difficult (or impossible) to produce, especially in the case of large data path models; even small data path models with many inputs are not made readily tractable by homomorphic reduction. The same difficulties applied in some degree to induction.

Significant in-roads into these difficulties have been made through the work on symbolic model checking using binary decision diagrams (BDD's), as introduced at the first session of this workshop in Grenoble (1989). While not scalable (effective use of BDD's currently appears to be limited to around 150 binary variables, while applications often require thousands), use of BDD's in conjunction with homomorphic reduction and induction appears extremely promising and has generated considerable excitement. Introduced at this same meeting was work on real-time verification, which continues to generate much interest, as well.

The current workshop (CAV '90) presents some very substantial progress using BDD's. As well, this workshop introduces reductions based upon partial order representation; these reductions offer a new potential for dealing with the tractability problem inherent in state-based models. Other papers presented here explore theorem-proving and proof-checking in controller verification, and the remaining papers present much vital work which continues and extends current verification methods.

We have witnessed a migration from theorem-proving to model-checking, and a recent renewed interest in proof-checking. This may represent the start of a swing back toward theorem-proving, especially through the combination of model-checking and symbolic techniques. If so we may expect more general theorem-proving to become integrated into existing verification tools, providing a basis for static and dynamic reasoning from the same platform.

For example, verification of a (dynamic) property of a model through expansion of the model state space of BDD evaluation may be simplified by exploiting a symmetry or inductive property in the model; the symmetry or inductive property upon which the simplification is based, may be verified though a (static) syntactic check on the model specification, using theorem-proving techniques.

Whatever the future may hold, our perception is that computer-aided verification has emerged from a polymorphous adolescence into a very exciting and promising adulthood.

Three more CAV workshops have been planned; the next will be held in Aalberg, Denmark in July 1991 under the direction of Kim Larsen.

We would like to thank the other members of the Steering Committee and the members of the CAV '90 Program Committee for their invaluable help in making his workshop a success. We are appreciative of DIMACS for their sponsorship of the workshop and the contribution of their facilities at Rutgers University for the duration of the workshop (June 18-21). In particular, we thank Pat Toci of DIMACS for her extensive work organizing and managing the entire on-site logistics of the workshop, and we thank Thelma Pickell of AT&T Bell Labatories for administrative management of the meeting.

Steering Committee: E. Clarke, R. Kurshan, A. Pnueli, J. Sifakis

Program Committee: H. Barringer, G. Bochmann, R. Bryant, C. Courcoubetis, S. Dasgupta, D. Dill, A. Emerson, R. Gerth, B. Gopinath, Z. Har'El, G. Holtzmann, G. Milne, R. Platek, P. Sistla, M. Stickel, C. Stirling, P. Wolper, M. Yoeli

E. M. Clarke
R. P. Kurshan
Program Co-Chair
CAV '90


        E.M. Clarke and R. P. Kurshan                              xi

Temporal Logic Model Checking:  Two Techniques for Avoiding
      the State Explosion Problem
        Edmund M. Clarke, Jr.                                       1

Automatic Verification of Extensions of Hardware Descriptions
        Hans Eveking                                                3

Using Partial-Order Semantics to Avoid the State Explosion 
      Problem in Asynchronous Systems
        David K. Probst and Hon F. Li                              15

A Stubborn Attack on State Explosion
        Antti Valmari                                              25

PAPETRI: Environment for the Analysis of PETRI Nets
        G. Berthelot, C. Johnen, and L. Petrucci                   43

Compositional Minimization of Finite State Systems
        Susanne Graf and Bernhard Steffen                          57

Verifying Temporal Properties of Sequential Machines
      without Building Their State Diagrams
        Olivier Coudert, Jean Christophe Madre, 
          and Christian Berthet                                    75

Minimal Model Generation
        A. Bouajjani, J-C. Fernandez, and N. Halbwachs             85

Verifying Liveness Properties by Verifying Safety Properties
        Jerry R. Burch                                             93

Extension of the Karp and Miller Procedure to LOTOS
        Michel Barbeau and Gregor V. Bochmann                     103

Formal Verification of Digital Circuits Using Symbolic 
      Ternary System Models
        Randal E. Bryant and Caro-Johan H. Seger                  121

An Algebra for Delay-Insensitive Circuits
        Mark B. Josephs and Jan Tijmen Udding                     147

Synthesizing Processes and Schedulers from Temporal Specifications
        Howard Wong-Toi and David L. Dill                         177

Verification of Multiprocessor Cache Protocol Using Simulation
      Relations and Higher-Order Logic
        Paul Loewenstein and David L. Dill                        187

Memory Efficient Algorithms for the Verification of Temporal
        C. Courcoubetis, M. Vardi, P. Wolper,
          and M. Yannakakis                                       207

Vectorized Model Checking for Computation Tree Logic
        Hiromi Hiraishi, Shintaro Meki, and Kiyoharu Hamaguchi     219

On Some Implementation of Optimal Simulations
        Ryszard Janicki and Maciej Koutny                         231

Finiteness Conditions and Structural Construction of Automata
     for All Process Algebras
        Eric Madelaine and Didier Vergamini                       275

A Computation Theory and Implementation of Sequential Hardware
        Carl Pixley                                               293

Using Partial Orders to Improve Automatic Verification Methods
        Patrice Godefroid                                         321

A Context Dependent Equivalence Relation between Kripke 
        Bernhard Josko                                            341

The Modular Framework of Computer-Aided Verification
        Gil Shurek and Orna Grumberg                              359

Tool Support for the Refinement Calculus
        D.A. Carrington and K.A. Robinson                         381

A Unified Approach to the Deadlock Detection Problem in 
      Networks of Communicating Finite State Machines
        Wuxu Peng and S. Purushothaman                            395

A Computer-Aided Verification Tool for Finite State 
      Controller Systems
        Mark Bickford and Mandayam Srivas                         405

Program Verification by Symbolic Execution of Hyperfinite 
      Ideal Machines
        James M. Morris and Mark Howard                           441

On Automatically Distinguishing Inequivalent Processes
        Rance Cleaveland                                          463

        Valerie Roy and Robert De Simone                          477

A Data Path Verifier for Register Transfer Level Using Temporal
      Logic Language Tokio
        Hiroshi Nakamura, Yuji Kukimoto, Masahiro Fujita,
        and Hidehiko Tanaka                                       493

Model Checking and Graph Theory in Sequential ATPG
        P. Camurati, M. Gilli, P. Prinetto, and M. Sonza Reorda   505

Compositional Design and Verification of Communication Protocols,
      Using Labelled PETRI Nets
        Jean Christophe Lloret, Pierre Azema, 
          and Francois Vernadat                                   519  
Liveness Analysis and the Automatic Generation of Concurrent 
        Ugo Buy and Robert Moll                                   535

Branching Time Regular Temporal Logic for Model Checking with
      Linear Time Complexity
        Kiyoharu Hamaguchi, Hiromi Hiraishi, and Shuzo Yajima     551

Issues Arising in the Analysis of L.O
        Linda Ness                                                565

Automated RTL Verification Based on Predicate Calculus
        M. Langevin                                               577

The Algebraic Feedback Product of Automata.  A State Machine
      Based Model of Concurrent Systems
        Victor Yodaiken                                           591

Results on the Interface between Formal Verification and ATPG
        Hyunwoo Cho, Gary Hachtel, Seh-Woong Jeong, 
          Bernard Plessier, Eric Schwarz, and Fabio Somenzi       615

Index Index of Volumes
DIMACS Homepage
Contacting the Center
Document last modified on October 28, 1998.