Computer Aided Verification : 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009, Proceedings / edited by Ahmed Bouajjani, Oded Maler.

Format:

Book

Contributor:

Bouajjani, Ahmed, editor.

Maler, O. (Oded), editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

LNCS sublibrary. Theoretical computer science and general issues ; SL 1, 5643.

Theoretical Computer Science and General Issues ; 5643

Language:

English

Subjects (All):

Computer programming.

Computer architecture.

Software engineering.

Computer logic.

Logic, Symbolic and mathematical.

Programming Techniques.

Computer System Implementation.

Software Engineering/Programming and Operating Systems.

Logics and Meanings of Programs.

Software Engineering.

Mathematical Logic and Formal Languages.

Local Subjects:

Programming Techniques.

Computer System Implementation.

Software Engineering/Programming and Operating Systems.

Logics and Meanings of Programs.

Software Engineering.

Mathematical Logic and Formal Languages.

Physical Description:

1 online resource (XV, 722 pages).

Edition:

First edition 2009.

Contained In:

Springer eBooks

Place of Publication:

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2009.

System Details:

text file PDF

Summary:

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.

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

Other Format:

Printed edition:

ISBN:

978-3-642-02658-4

9783642026584

Access Restriction:

Restricted for use by site license.