CAV 2010
58 papers
- A Dash of Fairness for Compositional Reasoning
- A Logical Product Approach to Zonotope Intersection
- A Model Checker for AADL
- A NuSMV Extension for Graded-CTL Model Checking
- ABC: An Academic Industrial-Strength Verification Tool
- Abstract Analysis of Symbolic Executions
- Achieving Distributed Control through Model Checking
- An Abstraction-Refinement Approach to Verification of Artificial Neural Networks
- Automated Assume-Guarantee Reasoning through Implicit Learning
- Automatic Generation of Inductive Invariants from High-Level Microarchitectural Models of Communication Fabrics
- Automatically Proving Linearizability
- Bounded Underapproximations
- Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems
- Comfusy: A Tool for Complete Functional Synthesis
- Constraint Solving for Program Verification: Theory and Practice by Example
- Contessa: Concurrency Testing Augmented with Symbolic Analysis
- Directed Proof Generation for Machine Code
- Dsolve: Safety Verification via Liquid Types
- Dynamic Cutoff Detection in Parameterized Concurrent Programs
- Efficient Emptiness Check for Timed Büchi Automata
- Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification
- Fast Acceleration of Ultimately Periodic Relations
- Fences in Weak Memory Models
- Generating Litmus Tests for Contrasting Memory Consistency Models
- Gist: A Solver for Probabilistic Games
- Global Reachability in Bounded Phase Multi-stack Pushdown Systems
- Invariant Synthesis for Programs Manipulating Lists with Unbounded Data
- Jtlv: A Framework for Developing Verification Algorithms
- LTSmin: Distributed and Symbolic Reachability
- Lazy Annotation for Program Testing and Verification
- Learning Component Interfaces with May and Must Abstractions
- Local Verification of Global Invariants in Concurrent Programs
- Measuring and Synthesizing Systems in Probabilistic Environments
- Memory Management in Concurrent Algorithms
- Merit: An Interpolating Model-Checker
- Model Checking of Linearizability of Concurrent List Implementations
- Model-Checking Parameterized Concurrent Programs Using Linear Interfaces
- On Array Theory of Bounded Elements
- PARAM: A Model Checker for Parametric Markov Models
- PESSOA: A Tool for Embedded Controller Synthesis
- Petruchio: From Dynamic Networks to Nets
- Policy Monitoring in First-Order Temporal Logic
- Quantifier Elimination by Lazy Model Enumeration
- Quantitative Information Flow: From Theory to Practice?
- RATSY - A New Requirements Analysis Tool with Synthesis
- Retrofitting Legacy Code for Security
- Robustness in the Presence of Liveness
- SPLIT: A Compositional LTL Verifier
- Safety Verification for Probabilistic Hybrid Systems
- Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing
- Symbolic Bounded Synthesis
- Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems
- Termination Analysis with Compositional Transition Invariants
- The Static Driver Verifier Research Platform
- There's Plenty of Room at the Bottom: Analyzing and Verifying Machine Code
- Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs
- Verifying Low-Level Implementations of High-Level Datatypes
- libalf: The Automata Learning Framework