CAV 2010 Accepted Papers

Quantifier elimination by lazy model enumeration
Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification
SPLIT: A Compositional LTL Verifier
A Dash of Fairness for Compositional Reasoning
Model Checking of Linearizability of Concurrent List Implementations
JTLV : A Framework for Developing Verification Algorithms
PARAM: A Model Checker for Parametric Markov Models
Model-checking parameterized concurrent programs using linear interfaces
Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs
Symbolic Bounded Synthesis
On Array Theory of Bounded Elements
An Abstraction-Refinement Approach to Verification of Artificial Neural Networks
Comfusy: A Tool for Complete Functional Synthesis
Simulation Subsumption in Ramsey-based Büchi Automata Universality and Inclusion Testing
Efficient Emptiness Check for Timed Büchi Automata
Automated Assume-Guarantee Reasoning through Implicit Learning
A Logical Product Approach to Zonotope Intersection
Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems
Achieving Distributed Control Through Model Checking
Petruchio: From Dynamic Networks to Nets
CONTESSA: Concurrency Testing Augmented with Symbolic Analysis
Fast Acceleration of Ultimately Periodic Relations
Invariant Synthesis for Programs Manipulating Lists with Unbounded Data
Dynamic Cutoff Detection in Parameterized Concurrent Programs
Automatically proving linearizability
Global Reachability in Bounded Phase Multi-Stack Pushdown Systems
Breach, A Simulation-based Toolbox for the Verification and  Parameter Synthesis of Hybrid Systems
Verifying Low-Level Implementations of High-Level Datatypes
Measuring and Synthesizing Systems in Probabilistic Environments
Local Verification of Global Invariants in Concurrent Programs
Automatic Generation of Inductive Invariants from High-Level Microarchitectural Models of Communication Fabrics
Learning Component Interfaces with May and Must Abstractions
Merit: an Interpolating Model-Checker
LTSMIN: Distributed and Symbolic Reachability
Generating Litmus Tests for Contrasting Memory Consistency Models
Abstract Analysis of Symbolic Executions
PESSOA: A tool for embedded controller synthesis.
Dsolve: Verification Via Liquid Type Inference
Lazy Annotation for Program Testing and Verification
Safety Verification for Probabilistic Hybrid Systems