<div>====== CALL FOR PARTICIPATION ==================================================</div><div>24th International Conference on Computer Aided Verification (CAV 2012) </div><div>July 7-13, 2012 Berkeley, California, USA </div>
<div><br></div><div>Program Chairs: Madhusudan Parathasarathy and Sanjit A. Seshia</div><div>Website: <a href="http://cav12.cs.illinois.edu/">http://cav12.cs.illinois.edu/</a></div><div><br></div><div>Aims and Scope</div>
<div>--------------------------------------------------------------------------------</div><div><br></div><div>The conference on Computer Aided Verification (CAV), 2012, is the 24th in a</div><div>series dedicated to the advancement of the theory and practice of computer-aided</div>
<div>formal analysis methods for hardware and software systems. CAV considers it</div><div>vital to continue spurring advances in hardware and software verification while</div><div>expanding to new domains such as biological systems and computer security. The</div>
<div>conference covers the spectrum from theoretical results to concrete</div><div>applications, with an emphasis on practical verification tools and the</div><div>algorithms and techniques that are needed for their implementation. The</div>
<div>proceedings of the conference will be published in the Springer-Verlag Lecture</div><div>Notes in Computer Science series. A selection of papers will be invited to a</div><div>special issue of Formal Methods in System Design and the Journal of the ACM.</div>
<div><br></div><div>** NEW in 2012 **</div><div>--------------------------------------------------------------------------------</div><div>CAV will have *special tracks* in the following four areas:</div><div>1. Hardware Verification (track chair: Andreas Kuehlmann) </div>
<div>2. Computer Security (track chair: Somesh Jha) </div><div>3. Embedded Systems (track chair: Stavros Tripakis) </div><div>4. SAT and SMT (track chair: Daniel Kroening)</div><div><br></div><div><br></div><div>Invited Talks</div>
<div>--------------------------------------------------------------------------------</div><div>- Wolfgang Thomas, RWTH Aachen University </div><div> "Synthesis and Some of Its Challenges"</div><div><br></div><div>
- David Dill, Stanford University </div><div> "Model Checking Cell Biology"</div><div><br></div><div>- Alex Haldermann, University of Michigan</div><div> On security of voting machines</div><div><br></div><div>
Invited Tutorials</div><div>--------------------------------------------------------------------------------</div><div><br></div><div>- Rastislav Bodik and Emina Torlak, University of California, Berkeley </div><div> "Synthesizing Programs with Constraint Solvers"</div>
<div><br></div><div>- Aaron Bradley, University of Colorado at Boulder</div><div> "IC3 and Beyond: Incremental, Inductive Verification"</div><div><br></div><div>- Chris Myers, University of Utah </div><div> "Formal Verification of Genetic Circuits"</div>
<div><br></div><div>- Michał Moskal, Microsoft Research, Seattle </div><div> "From C to infinity and back: Unbounded auto-active verification with VCC"</div><div> </div><div><br></div><div>====== CONFERENCE PROGRAM ======================================================</div>
<div><br></div><div>Saturday July 7 - WORKSHOPS</div><div>----------------------------------------</div><div><br></div><div>- NSV 2012 5th International Workshop on Numerical Software Verification</div><div> Co-chairs: Swarat Chaudhuri, Sriram Sankaranarayanan</div>
<div><br></div><div>- (EC)^2 2012 Workshop on Exploiting Concurrency Efficiently and Correctly</div><div> Co-chairs: Sebastian Burckhardt, Azadeh Farzan, Ganesh Gopalakrishnan, </div><div> Stephen Siegel, Helmut Veith, Josef Widder</div>
<div><br></div><div>- SYNT 2012 1st Workshop on Synthesis </div><div> Co-chairs: Doron Peled, Sven Schewe</div><div><br></div><div>- AMFSB 2012 Applications of Formal Methods in Systems Biology </div><div> Co-chairs: Vincent Danos, Mahesh Viswanathan</div>
<div><br></div><div>- LfSA 2012 Logics for System Analysis </div><div> Co-chairs: André Platzer, Philipp Rümmer</div><div><br></div><div>Sunday July 8 - WORKSHOPS</div><div>----------------------------------------</div>
<div><br></div><div>- NSV 2012 5th International Workshop on Numerical Software Verification </div><div> Co-chairs: Swarat Chaudhuri, Sriram Sankaranarayanan</div><div><br></div><div>- (EC)^2 2012 Workshop on Exploiting Concurrency Efficiently and Correctly </div>
<div> Co-chairs: Sebastian Burckhardt, Azadeh Farzan, Ganesh Gopalakrishnan, </div><div> Stephen Siegel, Helmut Veith, Josef Widder</div><div><br></div><div>- SYNT 2012 1st Workshop on Synthesis </div><div> Co-chairs: Doron Peled, Sven Schewe</div>
<div><br></div><div>- AMFSB 2012 Applications of Formal Methods in Systems Biology </div><div> Co-chairs: Vincent Danos, Mahesh Viswanathan</div><div><br></div><div>- BOOGIE 2012 2nd International Workshop on Intermediate Verification Languages </div>
<div> Chair: Zvonimir Rakamaric</div><div><br></div><div>- REORDER 2012 First International Workshop on Memory Consistency Models </div><div> Co-chairs: Sela Mador-Haim, Jade Alglave</div><div><br></div><div>Monday July 9 - INVITED TUTORIALS</div>
<div>----------------------------------------</div><div><br></div><div> 8:30 - 10:00: "Synthesizing Programs with Constraint Solvers" (Ras Bodik and Emina Torlak) </div><div> 10:00 - 10:30: Break </div><div> 10:30 - 12:00: "IC3 and Beyond: Incremental, Inductive Verification" (Aaron Bradley)</div>
<div> 12:00 - 1:30: Break </div><div> 1:30 - 3:00: "Formal Verification of Genetic Circuits" (Chris Myers)</div><div> 3:00 - 3:30: Break</div><div> 3:30 - 5:00: "From C to infinity and back: Unbounded auto-active verification with VCC" (Michal Moskal)</div>
<div><br></div><div>Tuesday July 10</div><div>----------------------------------------</div><div><br></div><div> 8:30 - 9:00: Welcome </div><div> 9:00 - 10:00: "Synthesis and Some of Its Challenges" (Wolfgang Thomas - Keynote) </div>
<div> 10:00 - 10:30: Break</div><div> 10:30 - 12:00: AUTOMATA AND SYNTHESIS</div><div><br></div><div> R1 Jan Kretinsky and Javier Esparza</div><div> "Deterministic Automata for the (F,G)-fragment of LTL"</div>
<div><br></div><div> R2 Tomas Brazdil, Krishnendu Chatterjee, Antonin Kucera and Petr Novotny</div><div> "Efficient Controller Synthesis for Consumption Games with Multiple Resource Types"</div><div><br>
</div><div> R3 Rüdiger Ehlers</div><div> "ACTL ∩ LTL Synthesis"</div><div><br></div><div> T1 François Raskin</div><div> "Acacia+, a tool for LTL synthesis"</div><div><br></div><div>
T2 Chih-Hong Cheng, Michael Geisinger, Harald Ruess, Christian Buckl and Alois Knoll</div><div> "MGSyn: Automatic Synthesis for Industrial Automation"</div><div><br></div><div> 12:00 - 1:30: Break</div>
<div> 1:30 - 3:35: INDUCTIVE INFERENCE AND TERMINATION</div><div><br></div><div> R4 Yu-Fang Chen and Bow-Yaw Wang</div><div> "Learning Boolean Functions Incrementally"</div><div><br></div><div> R5 Rahul Sharma, Aditya Nori and Alex Aiken</div>
<div> "Interpolants as Classifiers"</div><div><br></div><div> R6 Wonchan Lee, Bow-Yaw Wang and Kwangkeun Yi</div><div> "Termination Analysis with Algorithmic Learning"</div><div><br></div>
<div> R7 Marc Brockschmidt, Richard Musiol, Carsten Otto and Jürgen Giesl</div><div> "Automated Termination Proofs for Java Programs with Cyclic Data"</div><div><br></div><div> R8 Javier Esparza, Andreas Gaiser and Stefan Kiefer</div>
<div> "Proving Termination of Probabilistic Programs Using Patterns"</div><div><br></div><div> 3:35 - 4:00: Break</div><div> 4:00 - 6:05: ABSTRACTION</div><div><br></div><div> R9 Arnaud Venet</div>
<div> "The Gauge Domain: Scalable Analysis of Linear Inequality Invariants"</div><div><br></div><div> R10 Josh Berdine, Arlen Cox, Samin Ishtiaq and Christoph Wintersteiger</div><div> "Diagnosing Abstraction Failure for Separation Logic-based Analyses"</div>
<div><br></div><div> R11 Aditya Thakur and Thomas Reps</div><div> "A Method for Symbolic Computation of Abstract Operations"</div><div><br></div><div> R12 Simone Fulvio Rollini, Ondrej Sery and Natasha Sharygina</div>
<div> "Leveraging Interpolant Strength in Model Checking"</div><div><br></div><div> T3 Evan Driscoll, Aditya Thakur and Thomas Reps</div><div> "OpenNWA: A Nested Word Automaton Library"</div>
<div><br></div><div> T4 Aws Albarghouthi, Yi Li, Arie Gurfinkel and Marsha Chechik</div><div> "UFO: A Framework for Abstraction- and Interpolation-Based Verification"</div><div><br></div><div> T5 Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise and Natasha Sharygina</div>
<div> "SAFARI: SMT-based Abstraction For Arrays with Interpolants"</div><div><br></div><div> 6:30 - 8:30: PC dinner</div><div><br></div><div>Wednesday July 11</div><div>----------------------------------------</div>
<div><br></div><div> 8:35 - 10:35: CONCURRENCY & SOFTWARE VERIFICATION</div><div><br></div><div> R13 Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi and Akash Lal</div><div> "Detecting Fair Non-Termination in Multithreaded Programs"</div>
<div><br></div><div> R14 Vineet Kahlon and Chao Wang</div><div> "Lock Removal for Concurrent Trace Programs"</div><div><br></div><div> R15 Gerhard Schellhorn, John Derrick and Heike Wehrheim</div><div>
"How to prove algorithms linearisable"</div><div><br></div><div> R16 Anthony Widjaja Lin and Matthew Hague</div><div> "Synchronisation- and Reversal-Bounded Analysis of Multithreaded Programs with Counters"</div>
<div><br></div><div> R17 Alessandro Cimatti and Alberto Griggio</div><div> "Software Model Checking via IC3"</div><div><br></div><div> 10:35 - 11:00: Break</div><div> 11:00 - 12:00: "Model Checking Cell Biology" (David Dill - Keynote)</div>
<div> 12:00 - 1:30: Lunch</div><div> 1:30 - 3:00: BIOLOGY & PROBABILISTIC SYSTEMS</div><div><br></div><div> R18 Calin Guet, Ashutosh Gupta, Thomas A. Henzinger, Maria Mateescu and Ali Sezgin</div><div> "Delayed Continuous Time Markov Chains for Genetic Regulatory Circuits"</div>
<div> </div><div> R19 Anvesh Komuravelli, Corina S. Pasareanu and Edmund M. Clarke</div><div> "Assume-Guarantee Abstraction Refinement for Probabilistic Systems"</div><div><br></div><div> R20 Cyrille Jegourel, Axel Legay and Sean Sedwards</div>
<div> "Cross entropy optimisation of importance sampling parameters for statistical model checking"</div><div><br></div><div> T6 David Benque, Sam Bourton, Caitlin Cockerton, Byron Cook, Jasmin Fisher,</div>
<div> Samin Ishtiaq, Nir Piterman, Alex Taylor and Moshe Vardi</div><div> "Ripple: Visual Tool for Modeling and Analysis of Biological Networks"</div><div><br></div><div> T7 Stefan Kiefer, Andrzej Murawski, Joel Ouaknine, Björn Wachter and James Worrell</div>
<div> "APEX: An analyzer for open probabilistic programs"</div><div><br></div><div> 3:30 - 4:00: Break</div><div> 4:00 - 5:30: *EMBEDDED AND CONTROL SYSTEMS* - special track session</div><div><br></div>
<div> R21 Adiya Zutshi, Sriram Sankaranarayanan and Ashish Tiwari</div><div> "Timed Relational Abstractions For Sampled Data Control Systems"</div><div><br></div><div> R22 Rupak Majumdar and Majid Zamani</div>
<div> "Approximately Bisimilar Symbolic Models for Digital Control Systems"</div><div><br></div><div> R23 Alessandro Cimatti, Raffaele Corvino, Armando Lazzaro, Iman Narasamdya, </div><div> Tiziana Rizzo, Marco Roveri, Angela Sanseviero and Andrei Tchaltsev</div>
<div> "Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System" </div><div><br></div><div> T8 Philip Armstrong, Joel Ouaknine, Hristina Palikareva and Bill Roscoe</div>
<div> "Recent Developments in FDR"</div><div><br></div><div> T9 Songzheng Song, Jun Sun, Yang Liu and Jin Song Dong</div><div> "A Model Checker for Hierarchical Probabilistic Real-time Systems"</div>
<div><br></div><div> 6:00 - 9:30: Banquet</div><div><br></div><div>Thursday July 12</div><div>----------------------------------------</div><div><br></div><div> 8:30 - 10:00: *SAT/SMT SOLVING AND SMT-BASED VERIFICATION* - special track session</div>
<div><br></div><div> R24 Isil Dillig, Thomas Dillig, Kenneth McMillan and Alex Aiken</div><div> "Minimum Satisfying Assignments for SMT"</div><div><br></div><div> R25 Cheng-Shen Han and Jie-Hong Roland Jiang</div>
<div> "When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way"</div><div><br></div><div> R26 Akash Lal, Shaz Qadeer and Shuvendu Lahiri</div><div> "Corral: A Solver for Reachability Modulo Theories"</div>
<div><br></div><div> T10 Shuvendu Lahiri, Chris Hawblitzel, Ming Kawaguchi and Henrique Rebêlo</div><div> "SymDiff: A language-agnostic semantic diff tool"</div><div><br></div><div> T11 Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout and Fatiha Zaidi</div>
<div> "Cubicle: A Parallel SMT-based Model Checker for Parameterized Systems"</div><div> </div><div><br></div><div> 10:00 - 10:30: Break</div><div> 10:30 - 12:00: *TIMED & HYBRID SYSTEMS* - special track session</div>
<div><br></div><div> R27 Shibashis Guha, Chinmay Narayan and S. Arun-Kumar</div><div> "On Decidability of Prebisimulation for Timed Automata"</div><div><br></div><div> R28 Ichiro Hasuo and Kohei Suenaga</div>
<div> "Exercises in Nonstandard Static Analysis of Hybrid Systems"</div><div><br></div><div> R29 Sergiy Bogomolov, Goran Frehse, Radu Grosu, Hamed Ladan, Andreas Podelski and Martin Wehrle</div><div> "A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceEx"</div>
<div><br></div><div> T12 Ashish Tiwari</div><div> "HybridSal Relational Abstracter"</div><div><br></div><div> T13 Swarat Chaudhuri and Armando Solar-Lezama</div><div> "Euler: A System for Numerical Optimization of Programs"</div>
<div><br></div><div> 12:00 - 1:30: Lunch</div><div> 1:30 - 2:45: *HARDWARE VERIFICATION* - special track session</div><div><br></div><div> R30 Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Scott Owens, Jade Alglave, Kayvan Memarian, </div>
<div> Rajeev Alur, Milo Martin, Peter Sewell and Derek Williams</div><div> "An Axiomatic Memory Model for Power Multiprocessors"</div><div><br></div><div> R31 Flavio M de Paula, Alan Hu and Amir Nahir</div>
<div> "nuTAB-BackSpace: Rewriting to Normalize Non-Determinism in Post-Silicon Debug Traces"</div><div><br></div><div> R32 Zyad Hassan, Aaron Bradley and Fabio Somenzi</div><div> "Incremental Inductive CTL Model Checking"</div>
<div><br></div><div> 2:45 - 3:35: Miscellaneous Tools</div><div><br></div><div> T14 Rishabh Singh and Armando Solar-Lezama</div><div> "SPT : Storyboard Programming Tool"</div><div><br></div><div> T15 Patrick Rondon, Ming Kawaguchi, Alexander Bakst and Ranjit Jhala</div>
<div> "CSolve: Verifying C With Liquid Types"</div><div><br></div><div> T16 Daniel Schwartz-Narbonne, Feng Liu, David August and Sharad Malik</div><div> "PASSERT: A tool for debugging parallel programs"</div>
<div><br></div><div> T17 Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas and Andrew E. Santosa</div><div> "TRACER: A Symbolic Execution Tool for Verification"</div><div><br></div><div> T18 Stephan Arlt and Martin Schäf</div>
<div> "Joogie: Infeasible Code Detection for Java"</div><div><br></div><div> T19 David Hopkins, Andrzej Murawski and Luke Ong</div><div> "Hector: An Equivalence Checker for a Higher-Order Fragment of ML"</div>
<div><br></div><div> T20 Jan Hoffmann, Klaus Aehlig and Martin Hofmann</div><div> "Resource Aware ML"</div><div><br></div><div> 3:35 - 4:00: Break</div><div> 4:00 - 5:30: Tool demo/poster session</div>
<div> 5:30 - 6:30: CAV business meeting</div><div> 6:30 - 9:00: SC dinner</div><div><br></div><div>Friday July 13</div><div>----------------------------------------</div><div><br></div><div> 9:00 - 10:00: On security of voting machines (Alex Haldermann - Invited talk)</div>
<div> 10:00 - 10:30: Break</div><div> 10:30 - 11:45: *SECURITY* - special track session</div><div><br></div><div> R33 Matt Fredrikson, Richard Joiner, Somesh Jha, Thomas Reps, Phillip Porras, </div><div> Hassen Saidi and Vinod Yegneswaran</div>
<div> "Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement"</div><div><br></div><div> R34 Boris Köpf, Laurent Mauborgne and Martín Ochoa</div><div> "Automatic Quantification of Cache Side-Channels"</div>
<div><br></div><div> R35 William Harris, Somesh Jha and Thomas Reps</div><div> "Secure Programming via Visibly Pushdown Safety Games"</div><div><br></div><div> 11:45 - 11:50: Mini-break</div><div> 11:50 - 1:05: VERIFICATION AND SYNTHESIS</div>
<div><br></div><div> R36 Nishant Sinha, Nimit Singhania, Satish Chandra and Manu Sridharan</div><div> "Alternate and Learn: Finding witnesses without looking all over"</div><div><br></div><div> R37 Duc Hiep Chu and Joxan Jaffar</div>
<div> "A Complete Method for Symmetry Reduction in Safety Verification"</div><div><br></div><div> R38 Rishabh Singh and Sumit Gulwani</div><div> "Synthesizing Number Transformations from Input-Output Examples"</div>
<div><br></div><div> 1:00 - 1:15: Conference Wrap-up</div><div><br></div>