Computer Aided Verification: 11th International Conference, CAV’99 Trento, Italy, July 6–10, 1999 Proceedings

Alternative Approaches to Hardware Verification....Pages 1-1
The Compositional Specification of Timed Systems — A Tutorial....Pages 2-7
Timed Automata....Pages 8-22
Ståalmarck’s Method with Extensions to Quantified Boolean Formulas....Pages 23-24
Verification of Parameterized Systems by Dynamic Induction....Pages 25-43
Formal Methods for Conformance Testing: Theory Can Be Practical....Pages 44-46
Proof of Correctness of a Processor with Reorder Buffer Using the Completion Functions Approach....Pages 47-59
Verifying Safety Properties of a PowerPC− Microprocessor Using Symbolic Model Checking without BDDs....Pages 60-71
Model Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High-Performance Netlists....Pages 72-83
Validation of Pipelined Processor Designs Using Esterel Tools: A Case Study....Pages 84-95
Automated Verification of a Parametric Real-Time Program: The ABR Conformance Protocol....Pages 96-107
Test Generation Derived from Model-Checking....Pages 108-122
Latency Insensitive Protocols....Pages 123-133
Handling Global Conditions in Parametrized System Verification....Pages 134-145
Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis....Pages 146-159
Experience with Predicate Abstraction....Pages 160-171
Model Checking of Safety Properties....Pages 172-183
A Complete Finite Prefix for Process Algebra....Pages 184-195
The Mathematical Foundation of Symbolic Trajectory Evaluation....Pages 196-207
Assume-Guarantee Refinement between Different Time Scales....Pages 208-221
Efficient Decision Procedures for Model Checking of Linear Time Logic Properties....Pages 222-235
Stutter-Invariant Languages, ω -Automata, and Temporal Logic....Pages 236-248
Improved Automata Generation for Linear Temporal Logic....Pages 249-260
On the Representation of Probabilities over Structured Domains....Pages 261-273
Model Checking Partial State Spaces with 3-Valued Temporal Logics....Pages 274-287
Elementary Microarchitecture Algebra....Pages 288-300
Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems....Pages 301-315
Stepwise CTL Model Checking of State/Event Systems....Pages 316-327
Optimizing Symbolic Model Checking for Constraint-Rich Models....Pages 328-340
Efficient Timed Reachability Analysis Using Clock Difference Diagrams....Pages 341-353
Mechanizing Proofs of Computation Equivalence....Pages 354-367
Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation....Pages 369-379
Automatic Verification of Combinational and Pipelined FFT Circuits....Pages 380-393
Efficient Analysis of Cyclic Definitions....Pages 394-405
A Theory of Restrictions for Logics and Automata....Pages 406-417
Model Checking Based on Sequential ATPG....Pages 418-430
Automatic Verification of Abstract State Machines....Pages 431-442
Abstract and Model Check while You Prove....Pages 443-454
Deciding Equality Formulas by Small Domains Instantiations....Pages 455-469
Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions....Pages 470-482
A Toolbox for the Analysis of Discrete Event Dynamic Systems....Pages 483-486
TIPPtool: Compositional Specification and Analysis of Markovian Performance Models....Pages 487-490
Java Bytecode Verification by Model Checking....Pages 491-494
NuSMV: A New Symbolic Model Verifier....Pages 495-499
PIL/SETHEO: A Tool for the Automatic Analysis of Authentication Protocols....Pages 500-503