Accepted Papers
CAV 2012 Accepted Papers
Regular Papers
Minimum Satisfying Assignments for SMT
Leveraging Interpolant Strength in Model Checking
Automatic Quantification of Cache Side-Channels
Delayed Continuous Time Markov Chains for Genetic Regulatory Circuits
How to prove algorithms linearisable
Automated Termination Proofs for Java Bytecode with Cyclic Data
A Box-based Distance between Regions for Guiding the Reachability Analysis of SpaceEx
Detecting Fair Non-Termination in Multithreaded Programs
Secure Programming via Visibly Pushdown Safety Games
When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way
Proving Termination of Probabilistic Programs Using Patterns
Interpolants as Classifiers
Timed Relational Abstractions For Sampled Data Control Systems
An Axiomatic Memory Model for Power Multiprocessors
On Decidability of Prebisimulation for Timed Automata
Software Model Checking via IC3
Scalable Bug Detection via Alternating Scope Expansion and Pertinent Scope Learning
Termination Analysis with Algorithmic Learning
A Method for Symbolic Computation of Abstract Operations
Efficient Controller Synthesis for Consumption Games with Multiple Resource Types
A Complete Method for Symmetry Reduction in Safety Verification
Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System
Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement
Cross entropy optimisation of importance sampling parameters for statistical model checking
Learning Boolean Functions Incrementally
Approximately Bisimilar Symbolic Models for Digital Control Systems
LTL ∩ ACTL Synthesis
Deterministic Automata for the (F,G)-fragment of LTL
The Gauge Domain: Scalable Analysis of Linear Inequality Invariants
Synchronisation- and Reversal-Bounded Analysis of Multithreaded Programs with Counters
Diagnosing Abstraction Failure for Separation Logic-based Analyses
Incremental Inductive CTL Model Checking
Corral: A Solver for Reachability Modulo Theories
Lock Removal for Concurrent Trace Programs
nuTAB-BackSpace: Rewriting to Normalize Non-Determinism in Post-Silicon Debug Traces
Assume-Guarantee Abstraction Refinement for Probabilistic Systems
Synthesizing Number Transformations from Input-Output Examples
Exercises in Nonstandard Static Analysis of Hybrid Systems
Tool papers
MGSyn: Automatic Synthesis for Industrial Automation
Acacia+, a tool for LTL synthesis
TRACER: A Symbolic Execution Tool for Verification
SAFARI: SMT-based Abstraction For Arrays with Interpolants
Resource Aware ML
PASSERT: A tool for debugging parallel programs
Joogie: Infeasible Code Detection for Java
APEX: An analyzer for open probabilistic programs
Hector: An Equivalence Checker for a Higher-Order Fragment of ML
OpenNWA: A Nested Word Automaton Library
A Model Checker for Hierarchical Probabilistic Real-time Systems
Cubicle: A Parallel SMT-based Model Checker for Parameterized Systems
Euler: A System for Numerical Optimization of Programs
Ripple: Visual Tool for Modeling and Analysis of Biological Networks
SymDiff: A language-agnostic semantic diff tool
HybridSal Relational Abstracter
CSolve: Low-Level Program Verification with Liquid Types
SPT : Storyboard Programming Tool
UFO: A Framework for Abstraction- and Interpolation-Based Verification
Recent Developments in FDR