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

Front Matter....Pages -
Policy Monitoring in First-Order Temporal Logic....Pages 1-18
Retrofitting Legacy Code for Security....Pages 19-19
Quantitative Information Flow: From Theory to Practice?....Pages 20-22
Memory Management in Concurrent Algorithms....Pages 23-23
ABC: An Academic Industrial-Strength Verification Tool....Pages 24-40
There’s Plenty of Room at the Bottom: Analyzing and Verifying Machine Code....Pages 41-56
Constraint Solving for Program Verification: Theory and Practice by Example....Pages 57-71
Invariant Synthesis for Programs Manipulating Lists with Unbounded Data....Pages 72-88
Termination Analysis with Compositional Transition Invariants....Pages 89-103
Lazy Annotation for Program Testing and Verification....Pages 104-118
The Static Driver Verifier Research Platform....Pages 119-122
Dsolve: Safety Verification via Liquid Types....Pages 123-126
 Contessa : Concurrency Testing Augmented with Symbolic Analysis....Pages 127-131
Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing....Pages 132-147
Efficient Emptiness Check for Timed Büchi Automata....Pages 148-161
 Merit : An Interpolating Model-Checker....Pages 162-166
Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems....Pages 167-170
 Jtlv : A Framework for Developing Verification Algorithms....Pages 171-174
Petruchio: From Dynamic Networks to Nets....Pages 175-179
Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems....Pages 180-195
Safety Verification for Probabilistic Hybrid Systems....Pages 196-211
A Logical Product Approach to Zonotope Intersection....Pages 212-226
Fast Acceleration of Ultimately Periodic Relations....Pages 227-242
An Abstraction-Refinement Approach to Verification of Artificial Neural Networks....Pages 243-257
Fences in Weak Memory Models....Pages 258-272
Generating Litmus Tests for Contrasting Memory Consistency Models....Pages 273-287
Directed Proof Generation for Machine Code....Pages 288-305
Verifying Low-Level Implementations of High-Level Datatypes....Pages 306-320
Automatic Generation of Inductive Invariants from High-Level Microarchitectural Models of Communication Fabrics....Pages 321-338
Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification....Pages 339-353
 LTSmin: Distributed and Symbolic Reachability....Pages 354-359
 libalf : The Automata Learning Framework....Pages 360-364
Symbolic Bounded Synthesis....Pages 365-379
Measuring and Synthesizing Systems in Probabilistic Environments....Pages 380-395
Achieving Distributed Control through Model Checking....Pages 396-409
Robustness in the Presence of Liveness....Pages 410-424
RATSY – A New Requirements Analysis Tool with Synthesis....Pages 425-429
 Comfusy : A Tool for Complete Functional Synthesis....Pages 430-433
Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs....Pages 434-449
Automatically Proving Linearizability....Pages 450-464
Model Checking of Linearizability of Concurrent List Implementations....Pages 465-479
Local Verification of Global Invariants in Concurrent Programs....Pages 480-494
Abstract Analysis of Symbolic Executions....Pages 495-510
Automated Assume-Guarantee Reasoning through Implicit Learning....Pages 511-526
Learning Component Interfaces with May and Must Abstractions....Pages 527-542
A Dash of Fairness for Compositional Reasoning....Pages 543-557
SPLIT: A Compositional LTL Verifier....Pages 558-561
A Model Checker for AADL....Pages 562-565
PESSOA: A Tool for Embedded Controller Synthesis....Pages 566-569
On Array Theory of Bounded Elements....Pages 570-584
Quantifier Elimination by Lazy Model Enumeration....Pages 585-599
Bounded Underapproximations....Pages 600-614
Global Reachability in Bounded Phase Multi-stack Pushdown Systems....Pages 615-628
Model-Checking Parameterized Concurrent Programs Using Linear Interfaces....Pages 629-644
Dynamic Cutoff Detection in Parameterized Concurrent Programs....Pages 645-659
 PARAM : A Model Checker for Parametric Markov Models....Pages 660-664
 Gist : A Solver for Probabilistic Games....Pages 665-669
A NuSMV Extension for Graded-CTL Model Checking....Pages 670-673
Back Matter....Pages -