Computer Aided Verification 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010, Proceedings
| Other Authors: | , , |
|---|---|
| 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:
- Invited Talks
- Policy Monitoring in First-Order Temporal Logic
- Retrofitting Legacy Code for Security
- Quantitative Information Flow: 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
- Abstract Analysis of Symbolic Executions
- Session 10. Compositional Reasoning
- Automated Assume-Guarantee Reasoning through Implicit Learning
- Learning Component Interfaces with May and Must Abstractions
- A Dash of Fairness for Compositional Reasoning
- SPLIT: 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
- Automatic Generation of Inductive Invariants from High-LevelMicroarchitectural Models of Communication Fabrics
- Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification
- Session 7. Tools
- LTSmin: 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
- Efficient Emptiness Check for Timed Büchi Automata
- Session 3. Tools
- Merit: 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