Computer Aided Verification: 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, ProceedingsThis book constitutes the refereed proceedings of the 16th International Conference on Computer Aided Verification, CAV 2004, held in Boston, MA, USA, in July 2004. 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. |
What people are saying - Write a review
We haven't found any reviews in the usual places.
Contents
| 1 | |
| 15 | |
Deductive Verification of Pipelined Machines | 31 |
A Formal Reduction for LockFree Parallel Algorithms | 44 |
An Efficiently Checkable ProofBased Formulation of Vacuity | 57 |
Termination of Linear Programs | 70 |
Symbolic Model Checking of Nonregular Properties | 83 |
Proving More Properties with Bounded Model Checking | 96 |
Verification via Structure Simulation | 281 |
Symbolic Parametric Safety Analysis of Linear Hybrid Systems | 295 |
AbstractionBased Satisfiability Solving of Presburger Arithmetic | 308 |
Widening Arithmetic Automata | 321 |
Why Model Checking Can Improve WCET Analysis | 334 |
Regular Model Checking for LTLMSO | 348 |
Image Computation in Infinite State Model Checking | 361 |
Abstract Regular Model Checking | 372 |
Parallel LTLX Model Checking of HighLevel Petri Nets | 109 |
Using Interface Refinement to Integrate Formal Verification | 122 |
Indexed Predicate Discovery for Unbounded System Verification | 135 |
Range Allocation for Separation Logic | 148 |
An Experimental Evaluation of Ground Decision Procedures | 162 |
Fast Decision Procedures | 175 |
Verifying ωRegular Properties of Markov Chains | 189 |
Statistical Model Checking of BlackBox Probabilistic Systems | 202 |
Compositional Specification and Model Checking in GSTE | 216 |
GSTE Is Partitioned Model Checking | 229 |
StuckFree Conformance | 242 |
Symbolic Simulation Model Checking and Abstraction with Partially | 255 |
Functional Dependency for Verification Reduction | 268 |
Global ModelChecking of InfiniteState Systems | 387 |
An Efficient Execution Verification Tool | 401 |
Verification of an Advanced mipsType OutofOrder | 414 |
Automatic Verification of Sequential Consistency for Unbounded | 427 |
Efficient Modeling of Embedded Memories in Bounded Model Checking | 440 |
Understanding Counterexamples with explain | 453 |
The HiVy Tool Set | 466 |
Model Checking the Logic of Knowledge | 479 |
The Mec 5 ModelChecker | 488 |
Formal Analysis of Java Programs in JavaFAN | 501 |
A New Implementation | 515 |
| 535 | |
Other editions - View all
Computer Aided Verification: 16th International Conference, CAV ..., Volume 16 Rajeev Alur No preview available - 2004 |
Common terms and phrases
abstract interpretation algorithm Alur and D.A. approach arithmetic assignment automata automaton benchmarks Boolean Boolean Functional cache checker Computer Aided Verification Computer Science concrete Conf configurations constraints construction corresponding counterexample D.A. Peled Eds decidable logic decision procedure defined denote efficient encoding example execution finite fixpoint formal formal verification function given graph GSTE implementation infinite initial input instruction integer interface invariant iterations labeled language Lemma linear LNCS loop M-net memory method model checking node NuSMV operator out-of-order execution path pipeline predicate abstraction Presburger arithmetic problem Proc processor proof propositional protocol prove reachability analysis refinement represents safety properties SAT solver satisfies Section semantics sequential sequential consistency simulation specification Springer Springer-Verlag structure techniques termination Theorem timeout tion tool transition relation transition system tuples UCLID valid values variables vector
Bibliographic information
| Title | Computer Aided Verification: 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings Volume 3114 of Lecture Notes in Computer Science |
| Editors | Rajeev Alur, Doron A. Peled |
| Edition | illustrated |
| Publisher | Springer, 2004 |
| ISBN | 3540278133, 9783540278139 |
| Length | 536 pages |
| Subjects | › › Computers / Artificial Intelligence / General Computers / Computer Architecture Computers / Computer Science Computers / Information Technology Computers / Logic Design Computers / Programming / General Computers / Software Development & Engineering / General Mathematics / Discrete Mathematics Mathematics / Logic |
| Export Citation | BiBTeX EndNote RefMan |