David L. Dill (auth.), Nicolas Halbwachs, Doron Peled (eds.)3540662022, 9783540662020
The 34 revised full papers presented were carefully reviewed and selected from a total of 107 submissions. Also included are six invited contributions and five tool presentations. The book is organized in topical sections on processor verification, protocol verification and testing, infinite state spaces, theory of verification, linear temporal logic, modeling of systems, symbolic model checking, theorem proving, automata-theoretic methods, and abstraction.
Table of contents :
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
Reviews
There are no reviews yet.