[SMT-LIB] CAV 2012: Call for Participation

Clark Barrett barrett at cs.nyu.edu
Wed May 23 11:43:35 EDT 2012


====== CALL FOR PARTICIPATION
==================================================
24th International Conference on Computer Aided Verification (CAV 2012)
July 7-13, 2012 Berkeley, California, USA

Program Chairs: Madhusudan Parathasarathy and Sanjit A. Seshia
Website: http://cav12.cs.illinois.edu/

Aims and Scope
--------------------------------------------------------------------------------

The conference on Computer Aided Verification (CAV), 2012, is the 24th in a
series dedicated to the advancement of the theory and practice of
computer-aided
formal analysis methods for hardware and software systems. CAV considers it
vital to continue spurring advances in hardware and software verification
while
expanding to new domains such as biological systems and computer security.
The
conference covers the spectrum from theoretical results to concrete
applications, with an emphasis on practical verification tools and the
algorithms and techniques that are needed for their implementation. The
proceedings of the conference will be published in the Springer-Verlag
Lecture
Notes in Computer Science series. A selection of papers will be invited to a
special issue of Formal Methods in System Design and the Journal of the ACM.

** NEW in 2012 **
--------------------------------------------------------------------------------
CAV will have *special tracks* in the following four areas:
1. Hardware Verification (track chair: Andreas Kuehlmann)
2. Computer Security  (track chair: Somesh Jha)
3. Embedded Systems (track chair: Stavros Tripakis)
4. SAT and SMT (track chair: Daniel Kroening)


Invited Talks
--------------------------------------------------------------------------------
- Wolfgang Thomas, RWTH Aachen University
  "Synthesis and Some of Its Challenges"

 - David Dill, Stanford University
  "Model Checking Cell Biology"

- Alex Haldermann, University of Michigan
  On security of voting machines

Invited Tutorials
--------------------------------------------------------------------------------

- Rastislav Bodik and Emina Torlak, University of California, Berkeley
  "Synthesizing Programs with Constraint Solvers"

- Aaron Bradley, University of Colorado at Boulder
  "IC3 and Beyond: Incremental, Inductive Verification"

- Chris Myers, University of Utah
  "Formal Verification of Genetic Circuits"

- Michał Moskal, Microsoft Research, Seattle
  "From C to infinity and back: Unbounded auto-active verification with VCC"


====== CONFERENCE PROGRAM
======================================================

Saturday July 7 - WORKSHOPS
----------------------------------------

- 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 - WORKSHOPS
----------------------------------------

- 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 - INVITED TUTORIALS
----------------------------------------

  8:30 - 10:00: "Synthesizing Programs with Constraint Solvers" (Ras Bodik
and Emina Torlak)
 10:00 - 10:30: Break
 10:30 - 12:00: "IC3 and Beyond: Incremental, Inductive Verification"
(Aaron Bradley)
 12:00 -  1:30: Break
  1:30 -  3:00: "Formal Verification of Genetic Circuits" (Chris Myers)
  3:00 -  3:30: Break
  3:30 -  5:00: "From C to infinity and back: Unbounded auto-active
verification with VCC" (Michal Moskal)

Tuesday July 10
----------------------------------------

  8:30 -  9:00: Welcome
  9:00 - 10:00: "Synthesis and Some of Its Challenges" (Wolfgang Thomas -
Keynote)
 10:00 - 10:30: Break
 10:30 - 12:00: AUTOMATA AND SYNTHESIS

    R1  Jan Kretinsky and Javier Esparza
        "Deterministic Automata for the (F,G)-fragment of LTL"

    R2  Tomas Brazdil, Krishnendu Chatterjee, Antonin Kucera and Petr
Novotny
        "Efficient Controller Synthesis for Consumption Games with Multiple
Resource Types"

    R3  Rüdiger Ehlers
        "ACTL ∩ LTL Synthesis"

    T1  François Raskin
        "Acacia+, a tool for LTL synthesis"

    T2  Chih-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

    R4  Yu-Fang Chen and Bow-Yaw Wang
        "Learning Boolean Functions Incrementally"

    R5  Rahul Sharma, Aditya Nori and Alex Aiken
        "Interpolants as Classifiers"

    R6  Wonchan Lee, Bow-Yaw Wang and Kwangkeun Yi
        "Termination Analysis with Algorithmic Learning"

     R7  Marc Brockschmidt, Richard Musiol, Carsten Otto and Jürgen Giesl
        "Automated Termination Proofs for Java Programs with Cyclic Data"

    R8  Javier Esparza, Andreas Gaiser and Stefan Kiefer
        "Proving Termination of Probabilistic Programs Using Patterns"

  3:35 -  4:00:  Break
  4:00 -  6:05:  ABSTRACTION

    R9  Arnaud Venet
        "The Gauge Domain: Scalable Analysis of Linear Inequality
Invariants"

    R10 Josh Berdine, Arlen Cox, Samin Ishtiaq and Christoph Wintersteiger
        "Diagnosing Abstraction Failure for Separation Logic-based Analyses"

    R11 Aditya Thakur and Thomas Reps
        "A Method for Symbolic Computation of Abstract Operations"

    R12 Simone Fulvio Rollini, Ondrej Sery and Natasha Sharygina
        "Leveraging Interpolant Strength in Model Checking"

    T3  Evan Driscoll, Aditya Thakur and Thomas Reps
        "OpenNWA: A Nested Word Automaton Library"

    T4  Aws Albarghouthi, Yi Li, Arie Gurfinkel and Marsha Chechik
        "UFO: A Framework for Abstraction- and Interpolation-Based
Verification"

    T5  Francesco 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

    R13 Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi and Akash Lal
        "Detecting Fair Non-Termination in Multithreaded Programs"

    R14 Vineet Kahlon and Chao Wang
        "Lock Removal for Concurrent Trace Programs"

    R15 Gerhard Schellhorn, John Derrick and Heike Wehrheim
        "How to prove algorithms linearisable"

    R16 Anthony Widjaja Lin and Matthew Hague
        "Synchronisation- and Reversal-Bounded Analysis of Multithreaded
Programs with Counters"

    R17 Alessandro 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)
 12:00 -  1:30: Lunch
  1:30 -  3:00:  BIOLOGY & PROBABILISTIC SYSTEMS

    R18 Calin Guet, Ashutosh Gupta, Thomas A. Henzinger, Maria Mateescu and
Ali Sezgin
        "Delayed Continuous Time Markov Chains for Genetic Regulatory
Circuits"

    R19 Anvesh Komuravelli, Corina S. Pasareanu and Edmund M. Clarke
        "Assume-Guarantee Abstraction Refinement for Probabilistic Systems"

    R20 Cyrille Jegourel, Axel Legay and Sean Sedwards
        "Cross entropy optimisation of importance sampling parameters for
statistical model checking"

    T6  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"

    T7  Stefan 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

    R21 Adiya Zutshi, Sriram Sankaranarayanan and Ashish Tiwari
        "Timed Relational Abstractions For Sampled Data Control Systems"

    R22 Rupak Majumdar and Majid Zamani
        "Approximately Bisimilar Symbolic Models for Digital Control
Systems"

    R23 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"

    T8  Philip Armstrong, Joel Ouaknine, Hristina Palikareva and Bill Roscoe
        "Recent Developments in FDR"

    T9  Songzheng 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
----------------------------------------

  8:30 - 10:00: *SAT/SMT SOLVING AND SMT-BASED VERIFICATION* - special
track session

    R24 Isil Dillig, Thomas Dillig, Kenneth McMillan and Alex Aiken
        "Minimum Satisfying Assignments for SMT"

    R25 Cheng-Shen Han and Jie-Hong Roland Jiang
        "When Boolean Satisfiability Meets Gaussian Elimination in a
Simplex Way"

    R26 Akash Lal, Shaz Qadeer and Shuvendu Lahiri
        "Corral: A Solver for Reachability Modulo Theories"

    T10 Shuvendu Lahiri, Chris Hawblitzel, Ming Kawaguchi and Henrique
Rebêlo
        "SymDiff: A language-agnostic semantic diff tool"

    T11 Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout and Fatiha
Zaidi
        "Cubicle: A Parallel SMT-based Model Checker for Parameterized
Systems"


 10:00 - 10:30:  Break
 10:30 - 12:00:  *TIMED & HYBRID SYSTEMS* - special track session

    R27 Shibashis Guha, Chinmay Narayan and S. Arun-Kumar
        "On Decidability of Prebisimulation for Timed Automata"

    R28 Ichiro Hasuo and Kohei Suenaga
        "Exercises in Nonstandard Static Analysis of Hybrid Systems"

    R29 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"

    T12 Ashish Tiwari
        "HybridSal Relational Abstracter"

    T13 Swarat Chaudhuri and Armando Solar-Lezama
        "Euler: A System for Numerical Optimization of Programs"

 12:00 -  1:30: Lunch
  1:30 -  2:45: *HARDWARE VERIFICATION* - special track session

    R30 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"

    R31 Flavio M de Paula, Alan Hu and Amir Nahir
        "nuTAB-BackSpace: Rewriting to Normalize Non-Determinism in
Post-Silicon Debug Traces"

    R32 Zyad Hassan, Aaron Bradley and Fabio Somenzi
        "Incremental Inductive CTL Model Checking"

  2:45 -  3:35: Miscellaneous Tools

    T14 Rishabh Singh and Armando Solar-Lezama
        "SPT : Storyboard Programming Tool"

    T15 Patrick Rondon, Ming Kawaguchi, Alexander Bakst and Ranjit Jhala
        "CSolve: Verifying C With Liquid Types"

    T16 Daniel Schwartz-Narbonne, Feng Liu, David August and Sharad Malik
        "PASSERT: A tool for debugging parallel programs"

    T17 Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas and Andrew E.
Santosa
        "TRACER: A Symbolic Execution Tool for Verification"

    T18 Stephan Arlt and Martin Schäf
        "Joogie: Infeasible Code Detection for Java"

    T19 David Hopkins, Andrzej Murawski and Luke Ong
        "Hector: An Equivalence Checker for a Higher-Order Fragment of ML"

    T20 Jan Hoffmann, Klaus Aehlig and Martin Hofmann
        "Resource Aware ML"

  3:35 -  4:00: Break
  4:00 -  5:30: Tool demo/poster session
  5:30 -  6:30: CAV business meeting
  6:30 -  9:00: SC dinner

Friday July 13
----------------------------------------

  9:00 - 10:00: On security of voting machines (Alex Haldermann - Invited
talk)
 10:00 - 10:30:  Break
 10:30 - 11:45:  *SECURITY* - special track session

    R33 Matt Fredrikson, Richard Joiner, Somesh Jha, Thomas Reps, Phillip
Porras,
        Hassen Saidi and Vinod Yegneswaran
        "Efficient Runtime Policy Enforcement Using Counterexample-Guided
Abstraction Refinement"

    R34 Boris Köpf, Laurent Mauborgne and Martín Ochoa
        "Automatic Quantification of Cache Side-Channels"

    R35 William 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

    R36 Nishant Sinha, Nimit Singhania, Satish Chandra and Manu Sridharan
        "Alternate and Learn: Finding witnesses without looking all over"

    R37 Duc Hiep Chu and Joxan Jaffar
        "A Complete Method for Symmetry Reduction in Safety Verification"

    R38 Rishabh Singh and Sumit Gulwani
        "Synthesizing Number Transformations from Input-Output Examples"

  1:00 -  1:15:  Conference Wrap-up


More information about the SMT-LIB mailing list