Computer Aided Verification 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010, Proceedings

Corporate Author: SpringerLink (Online service)
Other Authors: Touili, Tayssir (Editor), Cook, Byron (Editor), Jackson, Paul (Editor)
Format: eBook
Language:English
Published: Berlin, Heidelberg Springer Berlin Heidelberg 2010, 2010
Edition:1st ed. 2010
Series:Theoretical Computer Science and General Issues
Subjects:
Online Access:
Collection: Springer eBooks 2005- - Collection details see MPG.ReNa
Table of Contents:
  • A Compositional LTL Verifier
  • Session 11. Tools
  • A Model Checker for AADL
  • PESSOA: A Tool for Embedded Controller Synthesis
  • Session 12. Decision Procedures
  • On Array Theory of Bounded Elements
  • Quantifier Elimination by Lazy Model Enumeration
  • Session 13. Concurrent Program Verification II
  • Bounded Underapproximations
  • Global Reachability in Bounded Phase Multi-stack Pushdown Systems
  • Model-Checking Parameterized Concurrent Programs Using Linear Interfaces
  • Dynamic Cutoff Detection in Parameterized Concurrent Programs
  • Session 14. Tools
  • PARAM: A Model Checker for Parametric Markov Models
  • Gist: A Solver for Probabilistic Games
  • A NuSMV Extension for Graded-CTL Model Checking
  • Distributed and Symbolic Reachability
  • libalf: The Automata Learning Framework
  • Session 8. Synthesis
  • Symbolic Bounded Synthesis
  • Measuring and Synthesizing Systems in Probabilistic Environments
  • Achieving Distributed Control through Model Checking
  • Robustness in the Presence of Liveness
  • RATSY – A New Requirements Analysis Tool with Synthesis
  • Comfusy: A Tool for Complete Functional Synthesis
  • Session 9. Concurrent Program Verification I
  • Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs
  • Automatically Proving Linearizability
  • Model Checking of Linearizability of Concurrent List Implementations
  • Local Verification of Global Invariants in Concurrent Programs
  • An Interpolating Model-Checker
  • Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems
  • Jtlv: A Framework for Developing Verification Algorithms
  • Petruchio: From Dynamic Networks to Nets
  • Session 4. Counter and Hybrid Systems Verification
  • Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems
  • Safety Verification for Probabilistic Hybrid Systems
  • A Logical Product Approach to Zonotope Intersection
  • Fast Acceleration of Ultimately Periodic Relations
  • An Abstraction-Refinement Approach to Verification of Artificial Neural Networks
  • Session 5. Memory Consistency
  • Fences in Weak Memory Models
  • Generating Litmus Tests for Contrasting Memory Consistency Models
  • Session 6. Verification of Hardware and Low Level Code
  • Directed Proof Generation for Machine Code
  • Verifying Low-Level Implementations of High-Level Datatypes
  • From Theory to Practice?
  • Memory Management in Concurrent Algorithms
  • Invited Tutorials
  • ABC: An Academic Industrial-Strength Verification Tool
  • There’s Plenty of Room at the Bottom: Analyzing and Verifying Machine Code
  • Constraint Solving for Program Verification: Theory and Practice by Example
  • Session 1. Software Model Checking
  • Invariant Synthesis for Programs Manipulating Lists with Unbounded Data
  • Termination Analysis with Compositional Transition Invariants
  • Lazy Annotation for Program Testing and Verification
  • The Static Driver Verifier Research Platform
  • Dsolve: Safety Verification via Liquid Types
  • Contessa: Concurrency Testing Augmented with Symbolic Analysis
  • Session 2. Model Checking and Automata
  • Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing