Computer Aided Verification: 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009, Proceedings (Lecture Notes in Computer Science (5643))

This book constitutes the refereed proceedings of the 21st International Conference on Computer Aided Verification, CAV 2009, held in Grenoble, France, in June/July 2009. The 36 revised full papers presented together with 16 tool papers and 4 invited talks and 4 invited tutorials were carefully reviewed and selected from 135 regular paper and 34 tool paper submissions. The papers are dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems; their scope ranges from theoretical results to concrete applications, with an emphasis on practical verification tools and the underlying algorithms and techniques. Front Matter....Pages - Transactional Memory: Glimmer of a Theory....Pages 1-15 Mixed-Signal System Verification: A High-Speed Link Example....Pages 16-16 Modelling Epigenetic Information Maintenance: A Kappa Tutorial....Pages 17-32 Component-Based Construction of Real-Time Systems in BIP....Pages 33-34 Models and Proofs of Protocol Security: A Progress Report....Pages 35-49 Predictability vs. Efficiency in the Multicore Era: Fight of Titans or Happy Ever after?....Pages 50-50 SPEED: Symbolic Complexity Bound Analysis....Pages 51-62 Regression Verification: Proving the Equivalence of Similar Programs....Pages 63-63 Symbolic Counter Abstraction for Concurrent Software....Pages 64-78 Priority Scheduling of Distributed Systems Based on Model Checking....Pages 79-93 Explaining Counterexamples Using Causality....Pages 94-108 Size-Change Termination, Monotonicity Constraints and Ranking Functions....Pages 109-123 Linear Functional Fixed-points....Pages 124-139 Better Quality in Synthesis through Quantitative Objectives....Pages 140-156 Automatic Verification of Integer Array Programs....Pages 157-172 Automated Analysis of Java Methods for Confidentiality....Pages 173-187 Requirements Validation for Hybrid Systems....Pages 188-203 Towards Performance Prediction of Compositional Models in Industrial GALS Designs....Pages 204-218 Image Computation for Polynomial Dynamical Systems Using the Bernstein Expansion....Pages 219-232 Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers....Pages 233-247 Meta-analysis for Atomicity Violations under Nested Locking....Pages 248-262 An Antichain Algorithm for LTL Realizability....Pages 263-277 On Extending Bounded Proofs to Inductive Proofs....Pages 278-290 Games through Nested Fixpoints....Pages 291-305 Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories....Pages 306-320 Software Transactional Memory on Relaxed Memory Models....Pages 321-336 Sliding Window Abstraction for Infinite Markov Chains....Pages 337-352 Centaur Technology Media Unit Verification....Pages 353-367 Incremental Instance Generation in Local Reasoning....Pages 368-382 Quantifier Elimination via Functional Composition....Pages 383-397 Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique....Pages 398-413 Replacing Testing with Formal Verification in Intel $^{\scriptsize\circledR}$ Core TM i7 Processor Execution Engine Validation....Pages 414-429 Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models....Pages 430-445 A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints....Pages 446-461 Generalizing DPLL to Richer Logics....Pages 462-476 Reducing Context-Bounded Concurrent Reachability to Sequential Reachability....Pages 477-492 Intra-module Inference....Pages 493-508 Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers....Pages 509-524 Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints....Pages 525-539 Reachability Analysis of Hybrid Systems Using Support Functions....Pages 540-554 Reducing Test Inputs Using Information Partitions....Pages 555-569 On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure....Pages 570-583 Cardinality Abstraction for Declarative Networking Applications....Pages 584-598 Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences....Pages 599-613 D-Finder: A Tool for Compositional Deadlock Detection and Verification....Pages 614-619 HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous Environment....Pages 620-626 The Zonotope Abstract Domain Taylor1+....Pages 627-633 InvGen: An Efficient Invariant Generator....Pages 634-640 INFAMY: An Infinite-State Markov Model Checker....Pages 641-647 Browser-Based Enforcement of Interface Contracts in Web Applications with BeepBeep....Pages 648-653 Homer : A Higher-Order Observational Equivalence Model checkER....Pages 654-660 Apron : A Library of Numerical Abstract Domains for Static Analysis....Pages 661-667 Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic....Pages 668-674 CalFuzzer : An Extensible Active Testing Framework for Concurrent Programs....Pages 675-681 MCMAS: A Model Checker for the Verification of Multi-Agent Systems....Pages 682-688 TASS: Timing Analyzer of Scenario-Based Specifications....Pages 689-695 Translation Validation: From Simulink to C....Pages 696-701 VS 3 : SMT Solvers for Program Verification....Pages 702-708 PAT: Towards Flexible Verification under Fairness....Pages 709-714 A Concurrent Portfolio Approach to SMT Solving....Pages 715-720 Back Matter....Pages - This book constitutes the proceedings of the 26th International Conference on Computer Aided Verification, CAV 2014, held as part of the Vienna Summer of Logic, VSL 2014, in Vienna, Austria, in July 2014.