Computer Aided Verification: 12th International Conference, CAV 2000 Chicago, IL, USA, July 15-19, 2000 Proceedings (Google eBook)

Front Cover
E. Allen Emerson, A. Prasad Sistla
Springer Science & Business Media, Jun 28, 2000 - Computers - 582 pages
0 Reviews
This volume contains the proceedings of the 12th International Conference on Computer Aided Veri?cation (CAV 2000) held in Chicago, Illinois, USA during 15-19 July 2000. The CAV conferences are devoted to the advancement of the theory and practice of formal methods for hardware and software veri?cation. The con- rence covers the spectrum from theoretical foundations to concrete applications, with an emphasis on veri?cation algorithms, methods, and tools together with techniques for their implementation. The conference has traditionally drawn contributions from both researchers and practitioners in academia and industry. This year 91 regular research papers were submitted out of which 35 were - cepted, while 14 brief tool papers were submitted, out of which 9 were accepted for presentation. CAV included two invited talks and a panel discussion. CAV also included a tutorial day with two invited tutorials. Many industrial companies have shown a serious interest in CAV, ranging from using the presented technologies in their business to developing and m- keting their own formal veri?cation tools. We are very proud of the support we receive from industry. CAV 2000 was sponsored by a number of generous andforward-lookingcompaniesandorganizationsincluding:CadenceDesign- stems, IBM Research, Intel, Lucent Technologies, Mentor Graphics, the Minerva Center for Veri?cation of Reactive Systems, Siemens, and Synopsys. TheCAVconferencewasfoundedbyitsSteeringCommittee:EdmundClarke (CMU), Bob Kurshan (Bell Labs), Amir Pnueli (Weizmann), and Joseph Sifakis (Verimag).
  

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

Invited Talks and Tutorials
1
Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits
20
An AutomataTheoretic Approach to Reasoning about InfiniteState
36
Automatic Verification of Parameterized Cache Coherence Protocols
53
Binary Reachability Analysis of Discrete Pushdown Timed Automata
69
Boolean Satisfiability with Transitivity Constraints
85
Bounded Model Construction for Monadic SecondOrder Logics
99
Building Circuits from Relations
113
Induction in Compositional Model Checking
312
Liveness and Acceleration in Parameterized Verification
328
Mechanical Verification of an Ideal Incremental ABR Conformance
344
Model Checking ContinuousTime Markov Chains by Transient Analysis
358
ModelChecking for Hybrid Systems by Quotienting and Constraints
373
Efficient Reachability Analysis for Verification
389
Regular Model Checking
403
Symbolic Techniques for Parametric Reasoning about Counter and Clock
419

Combining Decision Diagrams and SAT Procedures for Efficient Symbolic
124
On the Completeness of Compositional Reasoning
139
CounterexampleGuided Abstraction Refinement
154
Decision Procedures for Inductive Boolean Functions Based on Alternating
170
Detecting Errors Before Reaching Them
186
A Discrete Strategy Improvement Algorithm for Solving Parity Games
202
Distributing Timed Model Checking How the Search Order Matters
216
Efficient Algorithms for Model Checking Pushdown Systems
232
Efficient Biichi Automata from LTL Formulae
248
Efficient Detection of Global Properties in Distributed Systems Using
264
Efficient Reachability Analysis of Hierarchical Reactive Machines
280
Formal Verification of VLIW Microprocessors with Speculative Execution
296
Syntactic Program Transformations for Automatic Abstraction
435
TemporalLogic Queries
450
Are Timed Automata Updatable?
464
Tuning SAT Checkers for Bounded Model Checking
480
Unfoldings of Unbounded Petri Nets
495
Disjunctive Invariants for Easy
508
Verifying Advanced Microarchitectures that Support Speculation
521
Tool Papers
538
Integrating WS1S with PVS
548
The STATEMATE Verification Environment Making It Real
561
A LogicProgrammingBased Verification Toolset
576
Copyright

Common terms and phrases