Computer Aided Verification 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings /
| Συγγραφή απο Οργανισμό/Αρχή: | |
|---|---|
| Άλλοι συγγραφείς: | , , |
| Μορφή: | Ηλεκτρονική πηγή Ηλ. βιβλίο |
| Γλώσσα: | English |
| Έκδοση: |
Berlin, Heidelberg :
Springer Berlin Heidelberg,
2010.
|
| Σειρά: | Lecture Notes in Computer Science,
6174 |
| Θέματα: | |
| Διαθέσιμο Online: | Full Text via HEAL-Link |
Πίνακας περιεχομένων:
- 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
- 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
- Automatic Generation of Inductive Invariants from High-Level Microarchitectural 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
- 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.
