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. YoeliE. M. Clarke
Preface 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 Specifications 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 Properties 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 Equivalence Carl Pixley 293 Using Partial Orders to Improve Automatic Verification Methods Patrice Godefroid 321 A Context Dependent Equivalence Relation between Kripke Structures 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 Auto/Autograph 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 Programs 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