Session 1 9:00 - 10:30 |
Welcome Welcome
|
Coffee |
|
Session 2 11:00 - 12:30 |
Regular Model-checking Verifying Programs with 1-Selector-Linked
Structures in Regular Model Checking
Ahmed Bouajjani, Peter Habermehl, Pierre Moro (Univ. Paris VII, France) and Tomáš Vojnar (Brno Univ. of Technology, Czech Republic) Simulation-Based Iteration of Tree
Transducers
Parosh Aziz Abdulla (Uppsala Univ., Sweden), Axel Legay (Univ. of Liège, Belgium), Julien d'Orso (CRCCyN-UMR CNRS, France) and Ahmed Rezine (Uppsala Univ., Sweden) Using Language Inference to Verify
Omega-regular Properties
Abhay Vardhan, Koushik Sen, Mahesh Viswanathan and Gul Agha (Univ. of Illinois, Urbana-Champaign, USA) |
Lunch |
|
Session 3 14:30 - 16:30 |
Infinite state systems On-the-fly Reachability and Cycle Detection
for Recursive State Machines
Rajeev Alur, Swarat Chaudhuri (Univ. of Pennsylvania, Philadelphia, USA), Kousha Etessami (Univ. of Edinburgh, UK) and P. Madhusudan (Univ. of Pennsylvania, Philadelphia, USA) Empirically Efficient Verification for a
Class of Infinite-State Systems
Jesse Bingham and Alan J. Hu (Univ. of British Columbia, Vancouver, Canada) Context-Bounded Model Checking of Concurrent
Software
Shaz Qadeer and Jakob Rehof (Microsoft Research, Redmond, USA) A Generic Theorem Prover of CSP Refinement
Yoshinao Isobe (AIST, Tsukuba, Japan) and Markus Roggenbach (Univ. of Wales, Swansea, UK) |
Coffee |
|
Session 4 17:00 - 18:30 |
Abstract Interpretation Separating Fairness and Well-Foundedness for
the Analysis of Fair Discrete Systems
Amir Pnueli (NYU, USA), Andreas Podelski and Andrey Rybalchenko (MPI, Saarbrücken, Germany) An Abstract Interpretation-based Refinement
Algorithm for Strong Preservation
Francesco Ranzato and Francesco Tapparo (Univ. of Padova, Italy) Guarded Types for Program Understanding
Raghavan Komondoor (IBM T.J. Watson Research Center, Yorktown Heights, USA), G. Ramalingam (IBM India, Bangalore, India), Satish Chandra (IBM India Research Lab, New Delhi, India) and John Field (IBM T.J. Watson Research Center, Yorktown Heights, USA) |
Coffee |
|
Session 2 10:30 - 12:30 |
Tools presentations 1 jMoped: A Java Bytecode Checker Based on
Moped
Dejvuth Suwimonteerabuth, Stefan Schwoon and Javier Esparza (Univ. of Stuttgart, Germany) Java-MOP: A Monitoring Oriented Programming
Environment for Java
Feng Chen and Grigore Rosu (Univ. of Illinois, Urbana-Champaign, USA) JML-Testing-Tools: A Symbolic Animator for
JML Specifications using CLP
Frederic Dadeau, Fabrice Bouquet, Bruno Legeard and Mark Utting (LIFC, CNRS-INRIA, Besançon, France) jETI: A Tool for Remote Tool Integration
Ralf Nagel, Tiziana Margaria (Univ. of Göttingen, Germany) and Bernhard Steffen (Univ. of Dortmund, Germany) |
Lunch |
|
Session 3 14:30 - 16:30 |
Automata and logics A Note on On-The-Fly Verification Algorithms
Stefan Schwoon and Javier Esparza (Univ. of Stuttgart, Germany) Truly On-The-Fly LTL Model Checking
Stephan Merz, Moritz Hammer and Alexander Knapp (Ludwig-Maximilans Univ., Munich, Germany) Complementation Constructions for
Nondeterministic Automata on Infinite Words
Orna Kupferman (Hebrew Univ., Jerusalem, Israel) and Moshe Y. Vardi (Rice Univ., Houston, USA) Using BDDs to Decide CTL
Will Marrero (DePaul Univ., Chicago, USA) |
Coffee |
|
Session 4 17:00 - 18:30 |
Probabilistic systems, probabilistic
model-checking Model-checking Infinite-state Markov Chains
Anne Remke, Boudewijn Haverkort and Lucia Cloth (Univ. of Twente, Enschede, The Netherlands) Algorithmic Verification of Recursive
Probabilistic Systems
Kousha Etessami (Univ. of Edinburgh, UK) and Mihalis Yannakakis (Columbia Univ., New York, USA) Monte Carlo Model Checking
Radu Grosu and Scott Smolka (State Univ. of New York, Stony Brook, USA) |
Session 1 9:00 - 10:00 |
Unifying invited talk |
Coffee |
|
Lunch |
|
Session 3a 14:30 - 15:30 |
Unifying invited talk Esterel v7:
From Verified Formal Specification to Efficient Industrial Designs
Gérard Berry, Esterel Technologies, Villeneuve-Loubet, France |
Coffee |
|
Evening 19:30 for 20:00 |
Banquet Conference Dinner at the National Museum of
Scotland, Chambers Street, preceded by a reception.
When you enter the museum, the first sight is the magnificent Main Hall, with its elegant bird-cage design. Flooded with natural light, it provides a great sense of space and tranquillity, with fountains and fishponds. It is a major exhibit in its own right and contains many wonderful objects. During the dinner it will not be possible to see the exhibits of the museum, but here is what you will miss: Thirty-six galleries of varying sizes present artefacts from around the globe and natural history specimens. See everything from steamships to sculptures, Egypt to evolution, Dolly the Sheep to design classics and black holes to brown bears. |
Coffee |
|
Session 2 10:30 - 12:30 |
Satisfiability Efficient Conflict Analysis for Finding All
Satisfying Assignments of a Boolean Circuit
HoonSang Jin, HyoJung Han and Fabio Somenzi (Univ. of Colorado, Boulder, USA) Bounded Validity Checking of Interval
Duration Logic
Babita Sharma (IIT Bombay, India), Paritosh Pandya (Tata Institute, Mumbai, India) and Supratik Chakraborty (IIT Bombay, India) An Incremental and Layered Procedure for the
Satisfiability of Linear Arithmetic Logic
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti (ITC-IRST, Trento, Italy), Tommi Junttila (Helsinki Univ.of Technology, Finland), Peter van Rossum (ITC-IRST, Trento, Italy), Stephan Schulz (Univ. of Verona, Italy) and Roberto Sebastiani (Univ. of Trento, Italy) A two-tier Technique for Supporting
Quantifiers in a Lazily Proof-explicating Theorem Prover
Rustan Leino, Madan Musuvathi (Microsoft Research, Redmond, USA) and Xinming Ou (Princeton Univ., USA) |
Lunch |
|
Session 3a 14:30 - 15:30 |
Invited talk Applications of
Craig Interpolation in Model Checking
Ken McMillan, Cadence Berkeley Labs, USA Location: George Square Lecture Theatre |
Session 3 15:45 - 16:45 |
Testing Symbolic Test Selection Based on Approximate
Analysis
Bertrand Jeannet, Thierry Jéron, Vlad Rusu and Elena Zinovieva (IRISA, Rennes, France) Symstra: A Framework for Generating
Object-oriented Unit Tests using Symbolic Execution
Tao Xie (Univ. of Washington, Seattle, USA), Darko Marinov (MIT, Cambridge, USA), Wolfram Schulte (Microsoft Research, Redmond, USA) and David Notkin (Univ. of Washington, Seattle, USA) |
Coffee |
|
Session 4 17:15 - 18:45 |
Abstraction and reduction Dynamic Symmetry Reduction
E. Allen Emerson and Thomas Wahl (Univ. of Texas, Austin, USA) Localization and Register Sharing for
Predicate Abstraction
Franjo Ivancic, Himanshu Jain, Aarti Gupta and Malay K. Ganai (NEC Labs, Princeton, USA) On Some Transformation Invariants under
Retiming and Resynthesis
Jie-Hong Jiang (Univ. of California, Berkeley, USA) |
Coffee |
|
Session 2 10:30 - 12:30 |
Specification, program synthesis Compositional Message Sequence Charts (CMSCs)
are better to Implement than MSCs
Blaise Genest (Univ. Paris VII, France and Warwick Univ., UK) Temporal Logic for Scenario-Based
Specifications
Hillel Kugler (NYU, USA), David Harel (Weizmann Institute, Rehovot, Israel), Amir Pnueli (NYU, USA), Yuan Lu (Broadcom, San Jose, USA) and Yves Bontemps (Univ. of Namur, Belgium) Mining Temporal Specifications for Error
Detection
Westley Weimer and George C. Necula (Univ. of California, Berkeley, USA) A New Algorithm for Strategy Synthesis in LTL
Games
Aidan Harding, Mark Ryan (Univ. of Birmingham, UK) and Pierre-Yves Schobbens (Univ. of Namur, Belgium) |
Lunch |
|
Session 3 14:30 - 16:30 |
Tool presentations 2 FocusCheck: A Tool for Model Checking and
Debugging Sequential C Programs
Curtis W. Keller (Iowa State Univ., Ames, USA), Diptikalyan Saha (State Univ. of New York, Stony Brook, USA), Samik Basu (Iowa State Univ., Ames, USA) and Scott A. Smolka (State Univ. of New York, Stony Brook, USA) SATABS: SAT-based Predicate Abstraction for
ANSI-C
Edmund Clarke (Carnegie Mellon Univ., Pittsburgh, USA), Daniel Kroening (ETH Zürich, Switzerland), Natasha Sharygina and Karen Yorav (Carnegie Mellon Univ., Pittsburgh, USA) DiVer: SAT-based Model Checking Platform for
Verifying Large Scale Systems
Malay Ganai, Gupta Aarti and Ashar Pranav (NEC Labs, Princeton, USA) BISIMULATOR: A Modular Tool for On-the-Fly
Equivalence Checking
Damien Bergamini, Nicolas Descoubes, Christophe Joubert and Radu Mateescu (INRIA Rhône-Alpes, Saint Ismier, France) |
Coffee |
|
Session 4 17:00 - 18:30 |
Model-checking Shortest Counterexamples for Symbolic Model
Checking of LTL with Past
Viktor Schuppan (ETH Zürich, Switzerland) and Armin Biere (Johannes Kepler Univ., Linz, Austria) Snapshot Verification
Blaise Genest (Univ. of Warwick, UK), Dietrich Kuske (TU Dresden, Germany), Anca Muscholl (Univ. Paris VII, France) and Doron Peled (Univ. of Warwick, UK) Time-efficient Model Checking with Magnetic
Disk
Tonglaga Bao and Michael Jones (Brigham Young Univ., Provo, USA) |
Evening 19:30 |
Dinner Dinner at Jury's Inn, 43 Jeffrey Street.
The hotel is perfectly located in the heart of the old city, right
beside the Royal Mile.
|