Overview

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.

Full Product Details

Author:   Ahmed Bouajjani ,  Oded Maler
Publisher:   Springer-Verlag Berlin and Heidelberg GmbH & Co. KG
Imprint:   Springer-Verlag Berlin and Heidelberg GmbH & Co. K
Edition:   2009 ed.
Volume:   5643
Dimensions:   Width: 15.50cm , Height: 2.50cm , Length: 23.50cm
Weight:   1.116kg
ISBN:  

9783642026577

ISBN 10:   3642026575
Pages:   722
Publication Date:   19 June 2009
Audience:   College/higher education ,  Professional and scholarly ,  Postgraduate, Research & Scholarly ,  Professional & Vocational
Format:   Paperback
Publisher's Status:   Active
Availability:   In Print  
This item will be ordered in for you from one of our suppliers. Upon receipt, we will promptly dispatch it out to you. For in store availability, please contact us.

Table of Contents

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 CoreTMi7 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 Programswithin 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.

Reviews

Author Information

Tab Content 6

Author Website:  

Countries Available

All regions