Computer Aided Verification: 9th International Conference, CAV’97 Haifa, Israel, June 22–25, 1997 Proceedings

F. Erich Marschner (auth.), Orna Grumberg (eds.)3540631666, 9783540631668

This book constitutes the strictly refereed proceedings of the 9th International Conference on Computer Aided Verification, CAV ’97, held in Haifa, Israel, in June 1997.
The volume presents 34 revised full papers selected from a total of 84 submissions. Also included are 7 invited contributions as well as 12 tool descriptions. The volume is dedicated to the theory and practice of computer aided formal methods for software and hardware verification, with an emphasis on verification tools and algorithms and the techniques needed for their implementation. The book is a unique record documenting the recent progress in the area.

---

Table of contents :
Practical challenges for industrial formal verification tools….Pages 1-2
Formal verification of digital systems, from ASICs to HW/SW codesign — a pragmatic approach….Pages 3-6
The industrial success of verification tools based on stålmarck’s method….Pages 7-10
Formal verification — Applications & case studies….Pages 11-11
Automatic abstraction techniques for propositional μ -calculus model checking….Pages 12-23
A compositional rule for hardware design refinement….Pages 24-35
Module checking revisited….Pages 36-47
Using compositional preorders in the verification of sliding window protocol….Pages 48-59
An efficient decision procedure for the theory of fixed-sized bit-vectors….Pages 60-71
Construction of abstract state graphs with PVS….Pages 72-83
Verification of a chemical process leak test procedure….Pages 84-94
Automatic datapath extraction for efficient usage of HDD….Pages 95-106
An n log n algorithm for online BDD refinement….Pages 107-118
Weak bisimulation for fully probabilistic processes….Pages 119-130
Towards a mechanization of cryptographic protocol verification….Pages 131-142
Efficient model checking using tabled resolution….Pages 143-154
Containment of regular languages in non-regular timing diagram languages is decidable….Pages 155-166
An improved reachability analysis method for strongly linear hybrid systems (extended abstract)….Pages 167-178
Some progress in the symbolic verification of timed automata….Pages 179-190
STARI: A case study in compositional and hierarchical timing verification….Pages 191-201
A provably correct embedded verifier for the certification of safety critical software….Pages 202-213
Model checking in a microprocessor design project….Pages 214-225
Some thoughts on statecharts, 13 years later….Pages 226-231
On-the-fly model checking under fairness that exploits symmetry….Pages 232-243
Exploiting symmetry when verifying transistor-level circuits by symbolic trajectory evaluation….Pages 244-255
Parallelizing the Mur ϕ verifier….Pages 256-267
A new heuristic for bad cycle detection using BDDs….Pages 268-278
Efficient detection of vacuity in ACTL formulas….Pages 279-290
Model checking and transitive-closure logic….Pages 291-302
Boolean and 2-adic numbers based techniques for verifying synchronous designs….Pages 303-303
Programs with quasi-stable channels are effectively recognizable….Pages 304-315
Combining constraint solving and symbolic model checking for a class of systems with non-linear constraints….Pages 316-327
Relaxed visibility enhances partial order reduction….Pages 328-339
Partial-order reduction in symbolic state space exploration….Pages 340-351
Deadlock checking using net unfoldings….Pages 352-363
Trace table based approach for pipelined microprocessor verification….Pages 364-375
On combining formal and informal verification….Pages 376-387
Efficient modeling of memory arrays in symbolic simulation….Pages 388-399
Symbolic model checking of infinite state systems using presburger arithmetic….Pages 400-411
Parametrized verification of linear networks using automata as invariants….Pages 412-423
Symbolic model checking with rich assertional languages….Pages 424-435
The invariant checker: Automated deductive verification of reactive systems….Pages 436-439
The PEP tool….Pages 440-443
TermiLog: A system for checking termination of queries to logic programs….Pages 444-447
Mosel : A sound and efficient tool for M2L(Str)….Pages 448-451
The verus tool: A quantitative approach to the formal verification of real-time systems….Pages 452-455
Uppaal : Status & developments….Pages 456-459
HyTech : A model checker for hybrid systems….Pages 460-463
SMC: A symmetry based model checker for verification of liveness properties….Pages 464-467
μcke — Efficient μ-calculus model checking….Pages 468-471
Prod 3.2 An advanced tool for efficient reachability analysis….Pages 472-475
VeriSoft: A tool for the automatic analysis of concurrent reactive software….Pages 476-479
RuleBase: Model checking at IBM….Pages 480-483