+612 9045 4394
Computer Aided Verification : 9th International Conference, Cav'97, Haifa, Israel, June 22-25, 1997, Proceedings - Orna Grumberg

Computer Aided Verification

9th International Conference, Cav'97, Haifa, Israel, June 22-25, 1997, Proceedings

By: Orna Grumberg (Editor)

Paperback Published: 4th June 1997
ISBN: 9783540631668
Number Of Pages: 492

Share This Book:


or 4 easy payments of $39.60 with Learn more
Ships in 5 to 9 business days

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.

Practical challenges for industrial formal verification toolsp. 1
Formal verification of digital systems, from ASICs to HW/SW codesign - a pragmatic approachp. 3
The industrial success of verification tools based on Stalmarck's methodp. 7
Formal verification - application and case studiesp. 11
Automatic abstraction techniques for propositional mu-calculus model checkingp. 12
A compositional rule for hardware design refinementp. 24
Module checking revisitedp. 36
Using compositional preorders in the verification of sliding window protocolp. 48
An efficient decision procedure for the theory of fixed-sized bit-vectorsp. 60
Construction of abstract state graphs with PVSp. 72
Verification of a chemical process leak test procedurep. 84
Automatic datapath extraction for efficient usage of HDDp. 95
An n log n algorithm for online BDD refinementp. 107
Weak bisimulation for fully probabilistic processesp. 119
Towards a mechanization of cryptographic protocol verificationp. 131
Efficient model checking using tabled resolutionp. 143
Containment of regular languages in non-regular timing diagram languages is decidablep. 155
An improved reachability analysis method for strongly linear hybrid systemsp. 167
Some progress in the symbolic verification of timed automatap. 179
STARI: A case study in compositional and hierarchical timing verificationp. 191
A provably correct embedded verifier for the certification of safety critical softwarep. 202
Model checking in a microprocessor design projectp. 214
Some thoughts on statecharts, 13 years laterp. 226
On-the-fly model checking under fairness that exploits symmetryp. 232
Exploiting symmetry when verifying transistor-level circuits by symbolic trajectory evaluationp. 244
Parallelizing the Murphi verifierp. 256
A new heuristic for bad cycle detection using BDDsp. 268
Efficient detection of vacuity in ACTL formulasp. 279
Model checking and transitive-closure logicp. 291
Boolean and 2-adic numbers based techniques for verifying synchronous designsp. 303
Programs with quasi-stable channels are effectively recognizablep. 304
Combining constraint solving and symbolic model checking for a class of systems with non-linear constraintsp. 316
Relaxed visibility enhances partial order reductionp. 328
Partial-order reduction in symbolic state space explorationp. 340
Deadlock checking using net unfoldingsp. 352
Trace table based approach for pipelined microprocessor verificationp. 364
On combining formal and informal verificationp. 376
Efficient modeling of memory arrays in symbolic simulationp. 388
Symbolic model checking of infinite state systems using Presburger arithmeticp. 400
Parametrized verification of linear networks using automata as invariantsp. 412
Symbolic model checking with rich assertional languagesp. 424
The Invariant Checker: Automated deductive verification of reactive systemsp. 436
The PEP toolp. 440
TermiLog: A system for checking termination of queries to logic programsp. 444
MOSEL: A sound and efficient tool for M2L(Str)p. 448
The Verus Tool: A quantitative approach to the formal verification of real-time systemsp. 452
UPPAAL - Status and developmentsp. 456
HYTECH: A model checker for hybrid systemsp. 460
SMC: A symmetry based model checker for verification of liveness propertiesp. 464
mucke - efficient mu-calculus model checkingp. 468
prod 3.2 - An advanced tool for efficient reachability analysisp. 472
VeriSoft: A tool for the automatic analysis of concurrent reactive softwarep. 476
RuleBase: Model checking at IBMp. 480
Author Indexp. 485
Table of Contents provided by Blackwell. All Rights Reserved.

ISBN: 9783540631668
ISBN-10: 3540631666
Series: Lecture Notes in Computer Science
Audience: General
Format: Paperback
Language: English
Number Of Pages: 492
Published: 4th June 1997
Publisher: Springer-Verlag Berlin and Heidelberg Gmbh & Co. Kg
Country of Publication: DE
Dimensions (cm): 23.39 x 15.6  x 2.57
Weight (kg): 0.7