Computer Aided Verification: 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005. Proceedings

George C. Necula, Sumit Gulwani (auth.), Kousha Etessami, Sriram K. Rajamani (eds.)3540272313, 9783540272311

This volume contains the proceedings of the International Conference on Computer Aided Veri?cation (CAV), held in Edinburgh, Scotland, July 6–10, 2005. CAV 2005 was the seventeenth in a series of conferences dedicated to the advancement of the theory and practice of computer-assisted formal an- ysis methods for software and hardware systems. The conference covered the spectrum from theoretical results to concrete applications, with an emphasis on practical veri?cation tools and the algorithms and techniques that are needed for their implementation. We received 123 submissions for regular papers and 32 submissions for tool papers.Ofthesesubmissions,theProgramCommitteeselected32regularpapers and 16 tool papers, which formed the technical program of the conference. The conference had three invited talks, by Bob Bentley (Intel), Bud Mishra (NYU), and George C. Necula (UC Berkeley). The conference was preceded by a tutorial day, with two tutorials: – Automated Abstraction Re?nement, by Thomas Ball (Microsoft) and Ken McMillan (Cadence); and – Theory and Practice of Decision Procedures for Combinations of (First- Order) Theories, by Clark Barrett (NYU) and Cesare Tinelli (U Iowa). CAV 2005 had six a?liated workshops: – BMC 2005: 3rd Int. Workshop on Bounded Model Checking; – FATES 2005: 5th Workshop on Formal Approaches to Testing Software; – GDV 2005: 2nd Workshop on Games in Design and Veri?cation; – PDPAR 2005: 3rd Workshop on Pragmatics of Decision Procedures in – tomated Reasoning; – RV 2005: 5th Workshop on Runtime Veri?cation; and – SoftMC 2005: 3rd Workshop on Software Model Checking.

---

Table of contents :
Front Matter….Pages –
Randomized Algorithms for Program Analysis and Verification….Pages 1-1
Validating a Modern Microprocessor….Pages 2-4
Algorithmic Algebraic Model Checking I: Challenges from Systems Biology….Pages 5-19
SMT-COMP: Satisfiability Modulo Theories Competition….Pages 20-23
Predicate Abstraction via Symbolic Decision Procedures….Pages 24-38
Interpolant-Based Transition Relation Approximation….Pages 39-51
Concrete Model Checking with Abstract Matching and Refinement….Pages 52-66
Abstraction for Falsification….Pages 67-81
Bounded Model Checking of Concurrent Programs….Pages 82-97
Incremental and Complete Bounded Model Checking for Full PLTL….Pages 98-111
Abstraction Refinement for Bounded Model Checking….Pages 112-124
Symmetry Reduction in SAT-Based Model Checking….Pages 125-138
Saturn: A SAT-Based Tool for Bug Detection….Pages 139-143
JVer: A Java Verifier….Pages 144-147
Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework….Pages 148-152
Wolf – Bug Hunter for Concurrent Software Using Formal Methods….Pages 153-157
Model Checking x86 Executables with CodeSurfer/x86 and WPDS++….Pages 158-163
The ComFoRT Reasoning Framework….Pages 164-169
Formal Verification of Pentium ® 4 Components with Symbolic Simulation and Inductive Invariants….Pages 170-184
Formal Verification of Backward Compatibility of Microcode….Pages 185-198
Compositional Analysis of Floating-Point Linear Numerical Filters….Pages 199-212
Syntax-Driven Reachable State Space Construction of Synchronous Reactive Programs….Pages 213-225
Program Repair as a Game….Pages 226-238
Improved Probabilistic Models for 802.11 Protocol Verification….Pages 239-252
Probabilistic Verification for “Black-Box” Systems….Pages 253-265
On Statistical Model Checking of Stochastic Systems….Pages 266-280
The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications….Pages 281-285
The Orchids Intrusion Detection Tool….Pages 286-290
TVOC: A Translation Validator for Optimizing Compilers….Pages 291-295
Cogent: Accurate Theorem Proving for Program Verification….Pages 296-300
F-Soft : Software Verification Platform….Pages 301-306
Yet Another Decision Procedure for Equality Logic….Pages 307-320
DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic….Pages 321-334
Efficient Satisfiability Modulo Theories via Delayed Theory Combination….Pages 335-349
Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking….Pages 350-363
Efficient Monitoring of ω -Languages….Pages 364-378
Verification of Tree Updates for Optimization….Pages 379-393
Expand, Enlarge and Check… Made Efficient….Pages 394-407
IIV: An Invisible Invariant Verifier….Pages 408-412
Action Language Verifier, Extended….Pages 413-417
Romeo: A Tool for Analyzing Time Petri Nets….Pages 418-423
TRANSYT:A Tool for the Verification of Asynchronous Concurrent Systems….Pages 424-428
Ymer: A Statistical Model Checker….Pages 429-433
Extended Weighted Pushdown Systems….Pages 434-448
Incremental Algorithms for Inter-procedural Analysis of Safety Properties….Pages 449-461
A Policy Iteration Algorithm for Computing Fixed Points in Static Analysis of Programs….Pages 462-475
Data Structure Specifications via Local Equality Axioms….Pages 476-490
Linear Ranking with Reachability….Pages 491-504
Reasoning About Threads Communicating via Locks….Pages 505-518
Abstraction Refinement via Inductive Learning….Pages 519-533
Automated Assume-Guarantee Reasoning for Simulation Conformance….Pages 534-547
Symbolic Compositional Verification by Learning Assumptions….Pages 548-562
Back Matter….Pages –