Doron Peled (auth.), Rajeev Alur, Doron A. Peled (eds.)3540223428, 9783540223429, 9783540278139
The 32 revised full research papers and 16 tool papers were carefully reviewed and selected from 144 submissions. The papers cover all current issues in computer aided verification and model checking, ranging from foundational and methodological issues to the evaluation of major tools and systems.
Table of contents :
Front Matter….Pages –
Rob Tristan Gerth: 1956–2003….Pages 1-14
Static Program Analysis via 3-Valued Logic….Pages 15-30
Deductive Verification of Pipelined Machines Using First-Order Quantification….Pages 31-43
A Formal Reduction for Lock-Free Parallel Algorithms….Pages 44-56
An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking….Pages 57-69
Termination of Linear Programs….Pages 70-82
Symbolic Model Checking of Non-regular Properties….Pages 83-95
Proving More Properties with Bounded Model Checking….Pages 96-108
Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings….Pages 109-121
Using Interface Refinement to Integrate Formal Verification into the Design Cycle….Pages 122-134
Indexed Predicate Discovery for Unbounded System Verification….Pages 135-147
Range Allocation for Separation Logic….Pages 148-161
An Experimental Evaluation of Ground Decision Procedures….Pages 162-174
DPLL( T ): Fast Decision Procedures….Pages 175-188
Verifying ω -Regular Properties of Markov Chains….Pages 189-201
Statistical Model Checking of Black-Box Probabilistic Systems….Pages 202-215
Compositional Specification and Model Checking in GSTE….Pages 216-228
GSTE Is Partitioned Model Checking….Pages 229-241
Stuck-Free Conformance….Pages 242-254
Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors….Pages 255-267
Functional Dependency for Verification Reduction….Pages 268-280
Verification via Structure Simulation….Pages 281-294
Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-Like Data-Structures….Pages 295-307
Abstraction-Based Satisfiability Solving of Presburger Arithmetic….Pages 308-320
Widening Arithmetic Automata….Pages 321-333
Why Model Checking Can Improve WCET Analysis….Pages 334-347
Regular Model Checking for LTL(MSO)….Pages 348-360
Image Computation in Infinite State Model Checking….Pages 361-371
Abstract Regular Model Checking….Pages 372-386
Global Model-Checking of Infinite-State Systems….Pages 387-400
QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings….Pages 401-413
Verification of an Advanced mips -Type Out-of-Order Execution Algorithm….Pages 414-426
Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values….Pages 427-439
Efficient Modeling of Embedded Memories in Bounded Model Checking….Pages 440-452
Understanding Counterexamples with explain ….Pages 453-456
Zapato : Automatic Theorem Proving for Predicate Abstraction Refinement….Pages 457-461
JNuke: Efficient Dynamic Analysis for Java….Pages 462-465
The HiVy Tool Set….Pages 466-469
ObsSlice : A Timed Automata Slicer Based on Observers….Pages 470-474
The UCLID Decision Procedure….Pages 475-478
MCK: Model Checking the Logic of Knowledge….Pages 479-483
Zing: A Model Checker for Concurrent Software….Pages 484-487
The Mec 5 Model-Checker….Pages 488-491
PlayGame: A Platform for Diagnostic Games….Pages 492-495
SAL 2….Pages 496-500
Formal Analysis of Java Programs in JavaFAN….Pages 501-505
A Toolset for Modelling and Verification of GALS Systems….Pages 506-509
WSAT: A Tool for Formal Analysis of Web Services….Pages 510-514
CVC Lite: A New Implementation of the Cooperating Validity Checker….Pages 515-518
CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking….Pages 519-522
Mechanical Mathematical Methods for Microprocessor Verification….Pages 523-533
Back Matter….Pages –
Reviews
There are no reviews yet.