Discrete Mathematics and Theoretical Computer Science
VOLUME THREE:
"COMPUTER-AIDED VERIFICATION '90"
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.
PREFACE
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. ClarkeR. P. Kurshan
Program Co-Chair
CAV '90
TABLE OF CONTENTS
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
Index of Volumes
DIMACS Homepage
Contacting the Center
Document last modified on October 28, 1998.