CAV 2012
64 papers
- A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceEx
- A Complete Method for Symmetry Reduction in Safety Verification
- A Method for Symbolic Computation of Abstract Operations
- A Model Checker for Hierarchical Probabilistic Real-Time Systems
- A Solver for Reachability Modulo Theories
- ACTL ∩ LTL Synthesis
- APEX: An Analyzer for Open Probabilistic Programs
- Acacia+, a Tool for LTL Synthesis
- Alternate and Learn: Finding Witnesses without Looking All over
- An Axiomatic Memory Model for POWER Multiprocessors
- Approximately Bisimilar Symbolic Models for Digital Control Systems
- Assume-Guarantee Abstraction Refinement for Probabilistic Systems
- Automated Termination Proofs for Java Programs with Cyclic Data
- Automatic Quantification of Cache Side-Channels
- Bma: Visual Tool for Modeling and Analyzing Biological Networks
- CSolve: Verifying C with Liquid Types
- Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking
- Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems - Tool Paper
- Delayed Continuous-Time Markov Chains for Genetic Regulatory Circuits
- Detecting Fair Non-termination in Multithreaded Programs
- Deterministic Automata for the (F, G)-Fragment of LTL
- Diagnosing Abstraction Failure for Separation Logic-Based Analyses
- Efficient Controller Synthesis for Consumption Games with Multiple Resource Types
- Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement
- Euler: A System for Numerical Optimization of Programs
- Exercises in Nonstandard Static Analysis of Hybrid Systems
- Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System
- Formal Verification of Genetic Circuits
- From C to Infinity and Back: Unbounded Auto-active Verification with VCC
- Hector: An Equivalence Checker for a Higher-Order Fragment of ML
- How to Prove Algorithms Linearisable
- HybridSAL Relational Abstracter
- IC3 and beyond: Incremental, Inductive Verification
- Incremental, Inductive CTL Model Checking
- Interpolants as Classifiers
- Joogie: Infeasible Code Detection for Java
- Learning Boolean Functions Incrementally
- Leveraging Interpolant Strength in Model Checking
- Lock Removal for Concurrent Trace Programs
- MGSyn: Automatic Synthesis for Industrial Automation
- Minimum Satisfying Assignments for SMT
- Model Checking Cell Biology
- On Decidability of Prebisimulation for Timed Automata
- OpenNWA: A Nested-Word Automaton Library
- Proving Termination of Probabilistic Programs Using Patterns
- Recent Developments in FDR
- Resource Aware ML
- SAFARI: SMT-Based Abstraction for Arrays with Interpolants
- SPT: Storyboard Programming Tool
- SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs
- Secure Programming via Visibly Pushdown Safety Games
- Software Model Checking via IC3
- Synchronisation- and Reversal-Bounded Analysis of Multithreaded Programs with Counters
- Synthesis and Some of Its Challenges
- Synthesizing Number Transformations from Input-Output Examples
- Synthesizing Programs with Constraint Solvers
- TRACER: A Symbolic Execution Tool for Verification
- Termination Analysis with Algorithmic Learning
- The Gauge Domain: Scalable Analysis of Linear Inequality Invariants
- Timed Relational Abstractions for Sampled Data Control Systems
- Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification
- When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way
- nuTAB-BackSpace: Rewriting to Normalize Non-determinism in Post-silicon Debug Traces
- passert: A Tool for Debugging Parallel Programs