Computer Aided Verification: 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004. Proceedings

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 -