*** Early registration ends June 20 ***<div><br></div><div><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>  &quot;Synthesis and Some of Its Challenges&quot;</div><div><br></div><div>- David Dill, Stanford University </div><div>  &quot;Model Checking Cell Biology&quot;</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>  &quot;Synthesizing Programs with Constraint Solvers&quot;</div><div><br></div><div>- Aaron Bradley, University of Colorado at Boulder</div><div>  &quot;IC3 and Beyond: Incremental, Inductive Verification&quot;</div>
<div><br></div><div>- Chris Myers, University of Utah </div><div>  &quot;Formal Verification of Genetic Circuits&quot;</div><div><br></div><div>- Michał Moskal, Microsoft Research, Seattle </div><div>  &quot;From C to infinity and back: Unbounded auto-active verification with VCC&quot;</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: &quot;Synthesizing Programs with Constraint Solvers&quot; (Ras Bodik and Emina Torlak)  </div>
<div> 10:00 - 10:30: Break </div><div> 10:30 - 12:00: &quot;IC3 and Beyond: Incremental, Inductive Verification&quot; (Aaron Bradley)</div><div> 12:00 -  1:30: Break </div><div>  1:30 -  3:00: &quot;Formal Verification of Genetic Circuits&quot; (Chris Myers)</div>
<div>  3:00 -  3:30: Break</div><div>  3:30 -  5:00: &quot;From C to infinity and back: Unbounded auto-active verification with VCC&quot; (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: &quot;Synthesis and Some of Its Challenges&quot; (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>        &quot;Deterministic Automata for the (F,G)-fragment of LTL&quot;</div><div><br></div><div>    R2  Tomas Brazdil, Krishnendu Chatterjee, Antonin Kucera and Petr Novotny</div>
<div>        &quot;Efficient Controller Synthesis for Consumption Games with Multiple Resource Types&quot;</div><div><br></div><div>    R3  Rüdiger Ehlers</div><div>        &quot;ACTL ∩ LTL Synthesis&quot;</div><div><br></div>
<div>    T1  François Raskin</div><div>        &quot;Acacia+, a tool for LTL synthesis&quot;</div><div><br></div><div>    T2  Chih-Hong Cheng, Michael Geisinger, Harald Ruess, Christian Buckl and Alois Knoll</div><div>        &quot;MGSyn: Automatic Synthesis for Industrial Automation&quot;</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>        &quot;Learning Boolean Functions Incrementally&quot;</div>
<div><br></div><div>    R5  Rahul Sharma, Aditya Nori and Alex Aiken</div><div>        &quot;Interpolants as Classifiers&quot;</div><div><br></div><div>    R6  Wonchan Lee, Bow-Yaw Wang and Kwangkeun Yi</div><div>        &quot;Termination Analysis with Algorithmic Learning&quot;</div>
<div><br></div><div>    R7  Marc Brockschmidt, Richard Musiol, Carsten Otto and Jürgen Giesl</div><div>        &quot;Automated Termination Proofs for Java Programs with Cyclic Data&quot;</div><div><br></div><div>    R8  Javier Esparza, Andreas Gaiser and Stefan Kiefer</div>
<div>        &quot;Proving Termination of Probabilistic Programs Using Patterns&quot;</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>        &quot;The Gauge Domain: Scalable Analysis of Linear Inequality Invariants&quot;</div><div><br></div><div>    R10 Josh Berdine, Arlen Cox, Samin Ishtiaq and Christoph Wintersteiger</div><div>        &quot;Diagnosing Abstraction Failure for Separation Logic-based Analyses&quot;</div>
<div><br></div><div>    R11 Aditya Thakur and Thomas Reps</div><div>        &quot;A Method for Symbolic Computation of Abstract Operations&quot;</div><div><br></div><div>    R12 Simone Fulvio Rollini, Ondrej Sery and Natasha Sharygina</div>
<div>        &quot;Leveraging Interpolant Strength in Model Checking&quot;</div><div><br></div><div>    T3  Evan Driscoll, Aditya Thakur and Thomas Reps</div><div>        &quot;OpenNWA: A Nested Word Automaton Library&quot;</div>
<div><br></div><div>    T4  Aws Albarghouthi, Yi Li, Arie Gurfinkel and Marsha Chechik</div><div>        &quot;UFO: A Framework for Abstraction- and Interpolation-Based Verification&quot;</div><div><br></div><div>    T5  Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise and Natasha Sharygina</div>
<div>        &quot;SAFARI: SMT-based Abstraction For Arrays with Interpolants&quot;</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 &amp; SOFTWARE VERIFICATION</div><div><br></div><div>    R13 Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi and Akash Lal</div><div>        &quot;Detecting Fair Non-Termination in Multithreaded Programs&quot;</div>
<div><br></div><div>    R14 Vineet Kahlon and Chao Wang</div><div>        &quot;Lock Removal for Concurrent Trace Programs&quot;</div><div><br></div><div>    R15 Gerhard Schellhorn, John Derrick and Heike Wehrheim</div><div>
        &quot;How to prove algorithms linearisable&quot;</div><div><br></div><div>    R16 Anthony Widjaja Lin and Matthew Hague</div><div>        &quot;Synchronisation- and Reversal-Bounded Analysis of Multithreaded Programs with Counters&quot;</div>
<div><br></div><div>    R17 Alessandro Cimatti and Alberto Griggio</div><div>        &quot;Software Model Checking via IC3&quot;</div><div><br></div><div> 10:35 - 11:00:  Break</div><div> 11:00 - 12:00:  &quot;Model Checking Cell Biology&quot; (David Dill - Keynote)</div>
<div> 12:00 -  1:30: Lunch</div><div>  1:30 -  3:00:  BIOLOGY &amp; PROBABILISTIC SYSTEMS</div><div><br></div><div>    R18 Calin Guet, Ashutosh Gupta, Thomas A. Henzinger, Maria Mateescu and Ali Sezgin</div><div>        &quot;Delayed Continuous Time Markov Chains for Genetic Regulatory Circuits&quot;</div>
<div>    </div><div>    R19 Anvesh Komuravelli, Corina S. Pasareanu and Edmund M. Clarke</div><div>        &quot;Assume-Guarantee Abstraction Refinement for Probabilistic Systems&quot;</div><div><br></div><div>    R20 Cyrille Jegourel, Axel Legay and Sean Sedwards</div>
<div>        &quot;Cross entropy optimisation of importance sampling parameters for statistical model checking&quot;</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>        &quot;Ripple: Visual Tool for Modeling and Analysis of Biological Networks&quot;</div><div><br></div><div>    T7  Stefan Kiefer, Andrzej Murawski, Joel Ouaknine, Björn Wachter and James Worrell</div>
<div>        &quot;APEX: An analyzer for open probabilistic programs&quot;</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>        &quot;Timed Relational Abstractions For Sampled Data Control Systems&quot;</div><div><br></div><div>    R22 Rupak Majumdar and Majid Zamani</div>
<div>        &quot;Approximately Bisimilar Symbolic Models for Digital Control Systems&quot;</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>        &quot;Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System&quot;     </div><div><br></div><div>    T8  Philip Armstrong, Joel Ouaknine, Hristina Palikareva and Bill Roscoe</div>
<div>        &quot;Recent Developments in FDR&quot;</div><div><br></div><div>    T9  Songzheng Song, Jun Sun, Yang Liu and Jin Song Dong</div><div>        &quot;A Model Checker for Hierarchical Probabilistic Real-time Systems&quot;</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>        &quot;Minimum Satisfying Assignments for SMT&quot;</div><div><br></div><div>    R25 Cheng-Shen Han and Jie-Hong Roland Jiang</div>
<div>        &quot;When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way&quot;</div><div><br></div><div>    R26 Akash Lal, Shaz Qadeer and Shuvendu Lahiri</div><div>        &quot;Corral: A Solver for Reachability Modulo Theories&quot;</div>
<div><br></div><div>    T10 Shuvendu Lahiri, Chris Hawblitzel, Ming Kawaguchi and Henrique Rebêlo</div><div>        &quot;SymDiff: A language-agnostic semantic diff tool&quot;</div><div><br></div><div>    T11 Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout and Fatiha Zaidi</div>
<div>        &quot;Cubicle: A Parallel SMT-based Model Checker for Parameterized Systems&quot;</div><div>        </div><div><br></div><div> 10:00 - 10:30:  Break</div><div> 10:30 - 12:00:  *TIMED &amp; HYBRID SYSTEMS* - special track session</div>
<div><br></div><div>    R27 Shibashis Guha, Chinmay Narayan and S. Arun-Kumar</div><div>        &quot;On Decidability of Prebisimulation for Timed Automata&quot;</div><div><br></div><div>    R28 Ichiro Hasuo and Kohei Suenaga</div>
<div>        &quot;Exercises in Nonstandard Static Analysis of Hybrid Systems&quot;</div><div><br></div><div>    R29 Sergiy Bogomolov, Goran Frehse, Radu Grosu, Hamed Ladan, Andreas Podelski and Martin Wehrle</div><div>        &quot;A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceEx&quot;</div>
<div><br></div><div>    T12 Ashish Tiwari</div><div>        &quot;HybridSal Relational Abstracter&quot;</div><div><br></div><div>    T13 Swarat Chaudhuri and Armando Solar-Lezama</div><div>        &quot;Euler: A System for Numerical Optimization of Programs&quot;</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>        &quot;An Axiomatic Memory Model for Power Multiprocessors&quot;</div><div><br></div><div>    R31 Flavio M de Paula, Alan Hu and Amir Nahir</div>
<div>        &quot;nuTAB-BackSpace: Rewriting to Normalize Non-Determinism in Post-Silicon Debug Traces&quot;</div><div><br></div><div>    R32 Zyad Hassan, Aaron Bradley and Fabio Somenzi</div><div>        &quot;Incremental Inductive CTL Model Checking&quot;</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>        &quot;SPT : Storyboard Programming Tool&quot;</div><div><br></div><div>    T15 Patrick Rondon, Ming Kawaguchi, Alexander Bakst and Ranjit Jhala</div>
<div>        &quot;CSolve: Verifying C With Liquid Types&quot;</div><div><br></div><div>    T16 Daniel Schwartz-Narbonne, Feng Liu, David August and Sharad Malik</div><div>        &quot;PASSERT: A tool for debugging parallel programs&quot;</div>
<div><br></div><div>    T17 Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas and Andrew E. Santosa</div><div>        &quot;TRACER: A Symbolic Execution Tool for Verification&quot;</div><div><br></div><div>    T18 Stephan Arlt and Martin Schäf</div>
<div>        &quot;Joogie: Infeasible Code Detection for Java&quot;</div><div><br></div><div>    T19 David Hopkins, Andrzej Murawski and Luke Ong</div><div>        &quot;Hector: An Equivalence Checker for a Higher-Order Fragment of ML&quot;</div>
<div><br></div><div>    T20 Jan Hoffmann, Klaus Aehlig and Martin Hofmann</div><div>        &quot;Resource Aware ML&quot;</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>        &quot;Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement&quot;</div><div><br></div><div>    R34 Boris Köpf, Laurent Mauborgne and Martín Ochoa</div><div>        &quot;Automatic Quantification of Cache Side-Channels&quot;</div>
<div><br></div><div>    R35 William Harris, Somesh Jha and Thomas Reps</div><div>        &quot;Secure Programming via Visibly Pushdown Safety Games&quot;</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>        &quot;Alternate and Learn: Finding witnesses without looking all over&quot;</div><div><br></div><div>    R37 Duc Hiep Chu and Joxan Jaffar</div>
<div>        &quot;A Complete Method for Symmetry Reduction in Safety Verification&quot;</div><div><br></div><div>    R38 Rishabh Singh and Sumit Gulwani</div><div>        &quot;Synthesizing Number Transformations from Input-Output Examples&quot;</div>
<div><br></div><div>  1:00 -  1:15:  Conference Wrap-up</div></div><div><br></div>