Computer Aided Verification: 21st International Conference, CAV 2009, Grenoble, France, June 26-July 2, 2009, Proceedings

ISBN-13: 9783642026577 / Angielski / Miękka / 2009 / 740 str.

Ahmed Bouajjani

Opis

This volume contains the proceedings of the 21st International Conference on Computer-Aided Veri?cation (CAV) held in Grenoble, France, between June 28 and July 2, 2009. CAV is dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems. Its scope ranges from theoretical results to concrete applications, with an emphasis on practical veri?cation tools and the underlying algorithms and techniques. Everyinstanceofaconferenceisspecialinitsownway.ThisCAVisspecialfor at least two reasons: ?rst, it took place in Grenoble, the place where the CAV series started 20 years ago. Secondly, there was a particularly large number of paper submissions: 135 regular papers and 34 tool papers, summing up to 169 submissions. They all went through an active review process, with each submissionreviewedbyfourmembersoftheProgramCommittee.Wealsosought external reviews from experts in certain areas. Authors had the opportunity to respond to the initial reviews during an author response period. All these inputs wereusedbytheProgramCommitteeinselectinga?nalprogramwith36 regular papers and 16 tool papers. In addition to the presentation of these papers, the program included the following: - Four invited tutorials: - Rachid Guerraoui (EPFL Lausanne, Switzerland): Transactional M- ory: Glimmer of a Theory. - Jaeha Kim (Stanford, USA): Mixed-Signal System Veri?cation: A High- Speed Link Example. - Jean Krivine (Institut des Hautes Etudes Scienti?ques, France): M- elling Epigenetic Information Maintenance: A Kappa Tutorial. - JosephSifakis (CNRS-VERIMAG, France): Component-BasedConstr- tion of Real-Time Systems in BIP.

Spis treści

Invited Tutorials.- Transactional Memory: Glimmer of a Theory.- Mixed-Signal System Verification: A High-Speed Link Example.- Modelling Epigenetic Information Maintenance: A Kappa Tutorial.- Component-Based Construction of Real-Time Systems in BIP.- Invited Talks.- Models and Proofs of Protocol Security: A Progress Report.- Predictability vs. Efficiency in the Multicore Era: Fight of Titans or Happy Ever after?.- SPEED: Symbolic Complexity Bound Analysis.- Regression Verification: Proving the Equivalence of Similar Programs.- Regular Papers.- Symbolic Counter Abstraction for Concurrent Software.- Priority Scheduling of Distributed Systems Based on Model Checking.- Explaining Counterexamples Using Causality.- Size-Change Termination, Monotonicity Constraints and Ranking Functions.- Linear Functional Fixed-points.- Better Quality in Synthesis through Quantitative Objectives.- Automatic Verification of Integer Array Programs.- Automated Analysis of Java Methods for Confidentiality.- Requirements Validation for Hybrid Systems.- Towards Performance Prediction of Compositional Models in Industrial GALS Designs.- Image Computation for Polynomial Dynamical Systems Using the Bernstein Expansion.- Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers.- Meta-analysis for Atomicity Violations under Nested Locking.- An Antichain Algorithm for LTL Realizability.- On Extending Bounded Proofs to Inductive Proofs.- Games through Nested Fixpoints.- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories.- Software Transactional Memory on Relaxed Memory Models.- Sliding Window Abstraction for Infinite Markov Chains.- Centaur Technology Media Unit Verification.- Incremental Instance Generation in Local Reasoning.- Quantifier Elimination via Functional Composition.- Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique.- Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation.- Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models.- A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints.- Generalizing DPLL to Richer Logics.- Reducing Context-Bounded Concurrent Reachability to Sequential Reachability.- Intra-module Inference.- Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers.- Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints.- Reachability Analysis of Hybrid Systems Using Support Functions.- Reducing Test Inputs Using Information Partitions.- On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure.- Cardinality Abstraction for Declarative Networking Applications.- Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences.- Tool Papers.- D-Finder: A Tool for Compositional Deadlock Detection and Verification.- HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous Environment.- The Zonotope Abstract Domain Taylor1+.- InvGen: An Efficient Invariant Generator.- INFAMY: An Infinite-State Markov Model Checker.- Browser-Based Enforcement of Interface Contracts in Web Applications with BeepBeep.- Homer: A Higher-Order Observational Equivalence Model checkER.- Apron: A Library of Numerical Abstract Domains for Static Analysis.- Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic.- CalFuzzer: An Extensible Active Testing Framework for Concurrent Programs.- MCMAS: A Model Checker for the Verification of Multi-Agent Systems.- TASS: Timing Analyzer of Scenario-Based Specifications.- Translation Validation: From Simulink to C.- VS3: SMT Solvers for Program Verification.- PAT: Towards Flexible Verification under Fairness.- A Concurrent Portfolio Approach to SMT Solving.

Blurb

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.