Technical Program

Saturday July 7

NSV 2012 5th International Workshop on Numerical Software Verification Co-chairs: Swarat Chaudhuri, Sriram Sankaranarayanan
(EC)^2 2012 Workshop on Exploiting Concurrency Efficiently and Correctly Co-chairs: Sebastian Burckhardt, Azadeh Farzan,
Ganesh Gopalakrishnan, Stephen Siegel, Helmut Veith, Josef Widder
SYNT 2012 1st Workshop on Synthesis Co-chairs: Doron Peled, Sven Schewe
AMFSB 2012 Applications of Formal Methods in Systems Biology Co-chairs: Vincent Danos, Mahesh Viswanathan
LfSA 2012 Logics for System Analysis Co-chairs: André Platzer, Philipp Rümmer

Sunday July 8

NSV 2012 5th International Workshop on Numerical Software Verification Co-chairs: Swarat Chaudhuri, Sriram Sankaranarayanan
(EC)^2 2012 Workshop on Exploiting Concurrency Efficiently and Correctly Co-chairs: Sebastian Burckhardt, Azadeh Farzan,
Ganesh Gopalakrishnan, Stephen Siegel, Helmut Veith, Josef Widder
SYNT 2012 1st Workshop on Synthesis Co-chairs: Doron Peled, Sven Schewe
AMFSB 2012 Applications of Formal Methods in Systems Biology Co-chairs: Vincent Danos, Mahesh Viswanathan
BOOGIE 2012 2nd International Workshop on Intermediate Verification Languages Chair: Zvonimir Rakamaric
REORDER 2012 First International Workshop on Memory Consistency Models Co-chairs: Sela Mador-Haim, Jade Alglave

Monday July 9

  8:30 - 10:00:“Synthesizing Programs with Constraint Solvers” (Ras Bodik and Emina Torlak)
Chair: Shuvendu Lahiri
10:00 - 10:30:Break
10:30 - 12:00: “IC3 and Beyond: Incremental, Inductive Verification” (Aaron Bradley)
Chair: Natasha Sharygina
12:00 -   1:30:Break
  1:30 -   3:00: “Formal Verification of Genetic Circuits” (Chris Myers)
Chair: Sanjit A. Seshia
  3:00 -   3:30:Break
  3:30 -   5:00:“From C to infinity and back: Unbounded auto-active verification with VCC” (Michal Moskal)
Chair: Madhusudan Parthasarathy
  6:00CAV Reception

Tuesday July 10

  8:30 -   9:00:Welcome
  9:00 - 10:00:“Synthesis and Some of Its Challenges” (Wolfgang Thomas - Keynote)
Chair: Madhusudan Parthasarathy
10:00 - 10:30:Break
10:30 - 12:00:AUTOMATA AND SYNTHESIS - Chair: Roderick Bloem
R1Jan Kretinsky and Javier Esparza
Deterministic Automata for the (F,G)-fragment of LTL
R2Tomas Brazdil, Krishnendu Chatterjee, Antonin Kucera and Petr Novotny
Efficient Controller Synthesis for Consumption Games with Multiple Resource Types
R3Rüdiger Ehlers
ACTL ∩ LTL Synthesis
T1Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Naiyong Jin and Jean-François Raskin
Acacia+, a tool for LTL synthesis
T2Chih-Hong Cheng, Michael Geisinger, Harald Ruess, Christian Buckl and Alois Knoll
MGSyn: Automatic Synthesis for Industrial Automation
12:00 -   1:30:Break
  1:30 -   3:35:INDUCTIVE INFERENCE AND TERMINATION - Chair: Sriram Sankaranarayanan
R4Yu-Fang Chen and Bow-Yaw Wang
Learning Boolean Functions Incrementally
R5Rahul Sharma, Aditya Nori and Alex Aiken
Interpolants as Classifiers
R6Wonchan Lee, Bow-Yaw Wang and Kwangkeun Yi
Termination Analysis with Algorithmic Learning
R7Marc Brockschmidt, Richard Musiol, Carsten Otto and Jürgen Giesl
Automated Termination Proofs for Java Programs with Cyclic Data
R8Javier Esparza, Andreas Gaiser and Stefan Kiefer
Proving Termination of Probabilistic Programs Using Patterns
  3:35 -   4:00:Break
  4:00 -   6:05:ABSTRACTION - Chair: Thomas Dillig
R9Arnaud Venet
The Gauge Domain: Scalable Analysis of Linear Inequality Invariants
R10Josh Berdine, Arlen Cox, Samin Ishtiaq and Christoph Wintersteiger
Diagnosing Abstraction Failure for Separation Logic-based Analyses
R11Aditya Thakur and Thomas Reps
A Method for Symbolic Computation of Abstract Operations
R12Simone Fulvio Rollini, Ondrej Sery and Natasha Sharygina
Leveraging Interpolant Strength in Model Checking
T3Evan Driscoll, Aditya Thakur and Thomas Reps
OpenNWA: A Nested Word Automaton Library
T4Aws Albarghouthi, Yi Li, Arie Gurfinkel and Marsha Chechik
UFO: A Framework for Abstraction- and Interpolation-Based Verification
T5Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise and Natasha Sharygina
SAFARI: SMT-based Abstraction For Arrays with Interpolants
  6:30 -   8:30:PC dinner

Wednesday July 11

  8:35 - 10:35:CONCURRENCY & SOFTWARE VERIFICATION - Chair: Zvonimir Rakamaric
R13Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi and Akash Lal
Detecting Fair Non-Termination in Multithreaded Programs
R14Vineet Kahlon and Chao Wang
Lock Removal for Concurrent Trace Programs
R15Gerhard Schellhorn, John Derrick and Heike Wehrheim
How to prove algorithms linearisable
R16Anthony Widjaja Lin and Matthew Hague
Synchronisation- and Reversal-Bounded Analysis of Multithreaded Programs with Counters
R17Alessandro Cimatti and Alberto Griggio
Software Model Checking via IC3
10:35 - 11:00:Break
11:00 - 12:00:“Model Checking Cell Biology” (David Dill - Keynote)
Chair: Sanjit A. Seshia
12:00 -   1:30:Lunch
  1:30 -   3:00:BIOLOGY & PROBABILISTIC SYSTEMS - Chair: Mahesh Viswanathan
R18Calin Guet, Ashutosh Gupta, Thomas A. Henzinger, Maria Mateescu and Ali Sezgin
Delayed Continuous Time Markov Chains for Genetic Regulatory Circuits
R19Anvesh Komuravelli, Corina S. Pasareanu and Edmund M. Clarke
Assume-Guarantee Abstraction Refinement for Probabilistic Systems
R20Cyrille Jegourel, Axel Legay and Sean Sedwards
Cross entropy optimisation of importance sampling parameters for statistical model checking
T6David 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
T7Stefan Kiefer, Andrzej Murawski, Joel Ouaknine, Björn Wachter and James Worrell
APEX: An analyzer for open probabilistic programs
  3:30 -   4:00:Break
  4:00 -   5:30:*EMBEDDED AND CONTROL SYSTEMS* - special track session - Chair: Stavros Tripakis
R21Adiya Zutshi, Sriram Sankaranarayanan and Ashish Tiwari
Timed Relational Abstractions For Sampled Data Control Systems
R22Rupak Majumdar and Majid Zamani
Approximately Bisimilar Symbolic Models for Digital Control Systems
R23Alessandro 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
T8Philip Armstrong, Joel Ouaknine, Hristina Palikareva and Bill Roscoe
Recent Developments in FDR
T9Songzheng Song, Jun Sun, Yang Liu and Jin Song Dong
A Model Checker for Hierarchical Probabilistic Real-time Systems
  6:00 -   9:30:Banquet

Thursday July 12

  9:00 - 10:30:*SAT/SMT SOLVING AND SMT-BASED VERIFICATION* - special track session - Chair: Orna Grumberg
R24Isil Dillig, Thomas Dillig, Kenneth McMillan and Alex Aiken
Minimum Satisfying Assignments for SMT
R25Cheng-Shen Han and Jie-Hong Roland Jiang
When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way
R26Akash Lal, Shaz Qadeer and Shuvendu Lahiri
A Solver for Reachability Modulo Theories
T10Shuvendu Lahiri, Chris Hawblitzel, Ming Kawaguchi and Henrique Rebêlo
SymDiff: A language-agnostic semantic diff tool
T11Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout and Fatiha Zaidi
Cubicle: A Parallel SMT-based Model Checker for Parameterized Systems
10:30 - 11:00:Break
11:00 - 12:30:TIMED & HYBRID SYSTEMS - Chair: Rajeev Alur
R27Shibashis Guha, Chinmay Narayan and S. Arun-Kumar
On Decidability of Prebisimulation for Timed Automata
R28Ichiro Hasuo and Kohei Suenaga
Exercises in Nonstandard Static Analysis of Hybrid Systems
R29Sergiy 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
T12Ashish Tiwari
HybridSal Relational Abstracter
T13Swarat Chaudhuri and Armando Solar-Lezama
Euler: A System for Numerical Optimization of Programs
12:30 -   2:00:Lunch
 2:00 -   3:00:*HARDWARE VERIFICATION* - special track session - Chair: William Hung
R30Sela 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
R31Flavio M de Paula, Alan Hu and Amir Nahir
nuTAB-BackSpace: Rewriting to Normalize Non-Determinism in Post-Silicon Debug Traces
R32Zyad Hassan, Aaron Bradley and Fabio Somenzi
Incremental Inductive CTL Model Checking
 3:00 -   4:15:Miscellaneous Tools - Chair: Aarti Gupta
T14Rishabh Singh and Armando Solar-Lezama
SPT : Storyboard Programming Tool
T15Patrick Rondon, Ming Kawaguchi, Alexander Bakst and Ranjit Jhala
CSolve: Verifying C With Liquid Types
T16Daniel Schwartz-Narbonne, Feng Liu, David August and Sharad Malik
PASSERT: A tool for debugging parallel programs
T17Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas and Andrew E. Santosa
TRACER: A Symbolic Execution Tool for Verification
T18Stephan Arlt and Martin Schäf
Joogie: Infeasible Code Detection for Java
T19David Hopkins, Andrzej Murawski and Luke Ong
Hector: An Equivalence Checker for a Higher-Order Fragment of ML
T20Jan Hoffmann, Klaus Aehlig and Martin Hofmann
Resource Aware ML
 4:15 -   6:00:Tool demo/poster session
 6:00 -   7:00:CAV business meeting
 7:00 -   9:00:SC dinner

Friday July 13

  9:00 - 10:00:Verifiably Insecure: Perils and Prospects of Electronic Voting (Alex Haldermann - Invited talk)
Chair: Somesh Jha
10:00 - 10:30:Break
10:30 - 11:45:*SECURITY* - special track session - Chair: Swarat Chaudhuri
R33Matt Fredrikson, Richard Joiner, Somesh Jha, Thomas Reps, Phillip Porras, Hassen Saidi and Vinod Yegneswaran
Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement
R34Boris Köpf, Laurent Mauborgne and Martín Ochoa
Automatic Quantification of Cache Side-Channels
R35William Harris, Somesh Jha and Thomas Reps
Secure Programming via Visibly Pushdown Safety Games
11:45 - 11:50:Mini-break
11:50 -   1:05:VERIFICATION AND SYNTHESIS - Chair: Rupak Majumdar
R36Nishant Sinha, Nimit Singhania, Satish Chandra and Manu Sridharan
Alternate and Learn: Finding witnesses without looking all over
R37Duc Hiep Chu and Joxan Jaffar
A Complete Method for Symmetry Reduction in Safety Verification
R38Rishabh Singh and Sumit Gulwani
Synthesizing Number Transformations from Input-Output Examples
  1:00 -   1:15:Conference Wrap-up