Accepted Papers

CAV 2012 Accepted Papers

CAV 2012 Accepted Papers

Regular Papers

Isil Dillig, Thomas Dillig, Kenneth McMillan and Alex Aiken. Minimum Satisfying Assignments for SMT
Simone Fulvio Rollini, Ondrej Sery and Natasha Sharygina. Leveraging Interpolant Strength in Model Checking
Boris Köpf, Laurent Mauborgne and Martín Ochoa. Automatic Quantification of Cache Side-Channels
Calin Guet, Ashutosh Gupta, Thomas A. Henzinger, Maria Mateescu and Ali Sezgin. Delayed Continuous Time Markov Chains for Genetic Regulatory Circuits
Gerhard Schellhorn, John Derrick and Heike Wehrheim. How to prove algorithms linearisable
Marc Brockschmidt, Richard Musiol, Carsten Otto and Jürgen Giesl. Automated Termination Proofs for Java Bytecode with Cyclic Data
Sergiy Bogomolov, Goran Frehse, Radu Grosu, Hamed Ladan, Andreas Podelski and Martin Wehrle. A Box-based Distance between Regions for Guiding the Reachability Analysis of SpaceEx
Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi and Akash Lal. Detecting Fair Non-Termination in Multithreaded Programs
William Harris, Somesh Jha and Thomas Reps. Secure Programming via Visibly Pushdown Safety Games
Cheng-Shen Han and Jie-Hong Roland Jiang. When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way
Javier Esparza, Andreas Gaiser and Stefan Kiefer. Proving Termination of Probabilistic Programs Using Patterns
Rahul Sharma, Aditya Nori and Alex Aiken. Interpolants as Classifiers
Adiya Zutshi, Sriram Sankaranarayanan and Ashish Tiwari. Timed Relational Abstractions For Sampled Data Control Systems
Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Scott Owens, Jade Alglave, Kayvan Memarian, Rajeev Alur, Milo Martin, Peter Sewell and Derek Williams. An Axiomatic Memory Model for Power Multiprocessors
Shibashis Guha, Chinmay Narayan and S. Arun-Kumar. On Decidability of Prebisimulation for Timed Automata
Alessandro Cimatti and Alberto Griggio. Software Model Checking via IC3
Nishant Sinha, Nimit Singhania, Satish Chandra and Manu Sridharan. Scalable Bug Detection via Alternating Scope Expansion and Pertinent Scope Learning
Wonchan Lee, Bow-Yaw Wang and Kwangkeun Yi. Termination Analysis with Algorithmic Learning
Aditya Thakur and Thomas Reps. A Method for Symbolic Computation of Abstract Operations
Tomas Brazdil, Krishnendu Chatterjee, Antonin Kucera and Petr Novotny. Efficient Controller Synthesis for Consumption Games with Multiple Resource Types
Duc Hiep Chu and Joxan Jaffar. A Complete Method for Symmetry Reduction in Safety Verification
Alessandro Cimatti, Raffaele Corvino, Armando Lazzaro, Iman Narasamdya, Tiziana Rizzo, Marco Roveri, Angela Sanseviero and Andrei Tchaltsev. Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System
Matt Fredrikson, Richard Joiner, Somesh Jha, Thomas Reps, Phillip Porras, Hassen Saidi and Vinod Yegneswaran. Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement
Cyrille Jegourel, Axel Legay and Sean Sedwards. Cross entropy optimisation of importance sampling parameters for statistical model checking
Yu-Fang Chen and Bow-Yaw Wang. Learning Boolean Functions Incrementally
Rupak Majumdar and Majid Zamani. Approximately Bisimilar Symbolic Models for Digital Control Systems
Rüdiger Ehlers. LTL ∩ ACTL Synthesis
Jan Kretinsky and Javier Esparza. Deterministic Automata for the (F,G)-fragment of LTL
Arnaud Venet. The Gauge Domain: Scalable Analysis of Linear Inequality Invariants
Anthony Widjaja Lin and Matthew Hague. Synchronisation- and Reversal-Bounded Analysis of Multithreaded Programs with Counters
Josh Berdine, Arlen Cox, Samin Ishtiaq and Christoph Wintersteiger. Diagnosing Abstraction Failure for Separation Logic-based Analyses
Zyad Hassan, Aaron Bradley and Fabio Somenzi. Incremental Inductive CTL Model Checking
Akash Lal, Shaz Qadeer and Shuvendu Lahiri. Corral: A Solver for Reachability Modulo Theories
Vineet Kahlon and Chao Wang. Lock Removal for Concurrent Trace Programs
Flavio M de Paula, Alan Hu and Amir Nahir. nuTAB-BackSpace:  Rewriting to Normalize Non-Determinism in Post-Silicon Debug Traces
Anvesh Komuravelli, Corina S. Pasareanu and Edmund M. Clarke. Assume-Guarantee Abstraction Refinement for Probabilistic Systems
Rishabh Singh and Sumit Gulwani. Synthesizing Number Transformations from Input-Output Examples
Ichiro Hasuo and Kohei Suenaga. Exercises in Nonstandard Static Analysis of Hybrid Systems

Tool papers


Chih-Hong Cheng, Michael Geisinger, Harald Ruess, Christian Buckl and Alois Knoll. MGSyn: Automatic Synthesis for Industrial Automation
Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Naiyong Jin and Jean-François Raskin. Acacia+, a tool for LTL synthesis
Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas and Andrew E. Santosa. TRACER: A Symbolic Execution Tool for Verification
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise and Natasha Sharygina. SAFARI: SMT-based Abstraction For Arrays with Interpolants
Jan Hoffmann, Klaus Aehlig and Martin Hofmann. Resource Aware ML
Daniel Schwartz-Narbonne, Feng Liu, David August and Sharad Malik. PASSERT: A tool for debugging parallel programs
Stephan Arlt and Martin Schäf. Joogie: Infeasible Code Detection for Java
Stefan Kiefer, Andrzej Murawski, Joel Ouaknine, Björn Wachter and James Worrell. APEX: An analyzer for open probabilistic programs
David Hopkins, Andrzej Murawski and Luke Ong. Hector: An Equivalence Checker for a Higher-Order Fragment of ML
Evan Driscoll, Aditya Thakur and Thomas Reps. OpenNWA: A Nested Word Automaton Library
Songzheng Song, Jun Sun, Yang Liu and Jin Song Dong. A Model Checker for Hierarchical Probabilistic Real-time Systems
Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout and Fatiha Zaidi. Cubicle: A Parallel SMT-based Model Checker for Parameterized Systems
Swarat Chaudhuri and Armando Solar-Lezama. Euler: A System for Numerical Optimization of Programs
David Benque, Sam Bourton, Caitlin Cockerton, Byron Cook, Jasmin Fisher, Samin Ishtiaq, Nir Piterman, Alex Taylor and Moshe Vardi. Ripple: Visual Tool for Modeling and Analysis of Biological   Networks
Shuvendu Lahiri, Chris Hawblitzel, Ming Kawaguchi and Henrique Rebêlo. SymDiff: A language-agnostic semantic diff tool
Ashish Tiwari. HybridSal Relational Abstracter
Patrick Rondon, Ming Kawaguchi, Alexander Bakst and Ranjit Jhala. CSolve: Low-Level Program Verification with Liquid Types
Rishabh Singh and Armando Solar-Lezama. SPT : Storyboard Programming Tool
Aws Albarghouthi, Yi Li, Arie Gurfinkel and Marsha Chechik. UFO: A Framework for Abstraction- and Interpolation-Based Verification
Philip Armstrong, Joel Ouaknine, Hristina Palikareva and Bill Roscoe. Recent Developments in FDR