Monday 22 Oct Tutorial Day
Organizer: Rolf Drechsler, University of Bremen


Breakfast (registration from 8:15 to 8:45)
8:45-9:00 Welcome
9:00-10:30 Jasmin Fisher, Microsoft Research
Formal Methods in Cell Biology Abstract Slides
10:30-11:00 Coffee break

Torsten Schaub, University of Potsdam
Answer Set Programming Abstract

13:00-14:00 Lunch

Eric Feron, Guillaume Brat, Pierre-Loic Garoche, Pete Manolios, Marc Pantel.
Formal Methods for Areospace Applications Abstract

16:00-16:30 Coffee break
16:30-18:00 Alessandro Cimatti, Fondazione Bruno Kessler
Application of SMT solvers to hybrid system verification Abstract
18:30-20:30 Drinks Reception at Westminster College: Sponsored by Microsoft Research Cambridge.
We'll walk to Westminster after the last tutorial:

Tuesday 23 Oct Day 1
8:00 Breakfast (registration from 8:30 to 9:00)
8:50-9:00 Welcome by Ken Woodberry, Deputy Managing Director, Microsoft Research Cambridge

Keynote: Tony Hoare, Microsoft Research
Algebra of Concurrent Design Abstract Slides
Chair: Satnam Singh, Google, USA

10:00-10:30 Coffee break
Session 1: Concurrent Software Verification
Chair: Barbara Jobstmann, Jasper, Switzerland.

Efficient Predictive Analysis for Detecting Nondeterminism in Multi-Threaded Programs
Arnab Sinha, Sharad Malik and Aarti Gupta


Automatic Lock Insertion in Concurrent Programs
Vineet Kahlon

11:30-12:00 Multi-Pushdown Systems with Budgets
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Othmane Rezine and Jari Stenman.
12:00-13:30 Lunch
  Session 2: SAT and Model Checking Algorithms
Chair: Per Bjesse, Synopsys, USA
13:30-14:00 Quantifier Elimination by Dependency Sequents (Slides)
Eugene Goldberg and Panagiotis Manolios
14:00-14:30 Preprocessing Techniques for First-Order Clausification (Slides)
Krystof Hoder, Zurab Khasidashvili, Konstantin Korovin and Andrei Voronkov
14:30-15:00 A Liveness Checking Algorithm that Counts
Koen Claessen and Niklas Sorensson
15:00-15:30 Coffee break
  Session 3: Machine Code and Memory Verification
Chair: Pete Manolios
, Northeatern University, USA
15:30-16:00 A Formal Model of a Large Memory that Supports Efficient Execution (Slides)
Warren Hunt and Matt Kaufmann
16:00-16:30 Verification with Small and Short Worlds
Rohit Sinha, Cynthia Sturton, Petros Maniatis, Sanjit A. Seshia and David Wagner
16:30-16:45 Decompilation into Logic - Improved
Magnus O. Myreen, Michael J. C. Gordon and Konrad Slind
16:45-17:45 Business Meeting (open to all)

Tuesday 18:30-20:30:
ARM sponsored drinks at the Castle Inn:
You can walk into town from MSRC:

Wednesday 24 Oct Day 2
8:00-9:00 Breakfast (registration from 8:30 to 9:00)
Session 4: Formal Methods for Synthesis, Test and Debug
Chair: Alan Hu, UBC, Vancouver, Canada
9:00-9:30 Complete and Effective Robustness Checking by Means of Interpolation
Stefan Frehse, Goerschwin Fey, Eli Arbel, Karen Yorav and Rolf Drechsler
9:30-10:00 Symbolically Synthesizing Small Circuits (Slides)
Rudiger Ehlers, Robert Konighofer and Georg Hofferek
10:00-10:15 Automated Debugging of Missing Input Constraints in a Formal Verification Environment (Slides)
Brian Keng and Andreas Veneris
10:15-10:45 Coffee break
  Session 5: Software and Behavioural Hardware Verification
Chair: Koen Cleassen, Chalmers Technical University, Sweden
10:45-11:15 Algorithms for Software Model Checking: Predicate Abstraction vs. IMPACT (Slides)
Dirk Beyer and Philipp Wendler
11:15-11:45 Incremental Upgrade Checking by Means of Interpolation-based Function Summaries
Ondrej Sery, Grigory Fedyukovich and Natasha Sharygina
11:45-12:15 Verification of Parametric System Designs
Alessandro Cimatti, Iman Narasamdya and Marco Roveri
12:15-14:00 Lunch

Session 6: Formal Verification Techniques for Arithmetic Circuits and GPUs
Chair: Tom Melham, Oxford, UK

14:00-14:30 Deciding Floating-Point Logic with Systematic Abstraction
Leopold Haller, Alberto Griggio, Martin Brain and Daniel Kroening
14:30-15:00 Formal Verification of Error Correcting Circuits Using Computational Algebraic Geometry
Alexey Lvov, Luis Lastras, Viresh Paruthi, Robert Shadowen and Ali El-Zein
15:00-15:30 Symbolic Trajectory Evaluation: The Primary Validation Vehicle for Next Gen Intel Processor Graphics FPU
Achutha Kirankumar V M, Aarti Gupta and Rajnish Ghughal
15:30-16:00 Coffee break
16:00-17:00 Hardware Model-Checking Competition
17:00-19:00 Free time to travel to the banquet.
19:00-22:30 Banquet at Queens' Collegw:
You can walk to Queens' from MSRC:
Reception at 19:00, Meal at 19:30.

Thursday 25 Oct Day 3


Session 7: Automated Abstraction/Reduction Techniques
Chair: Mary Sheeran, Chalmers Technical University, Sweden

Enhanced Reachability Analysis via Automated Netlist-Based Hint Generation (Slides)
Jiazhao Xu, Mark Williams, Hari Mony and Jason Baumgartner

9:30- 10:00 Oscillator Verification with Probability One (Slides)
Chao Yan and Mark Greenstreet
10:00-10:30 Lazy Abstraction and SAT-based Reachability for Hardware Model Checking
Yakir Vizel, Orna Grumberg and Sharon Shoham Slides
10:30-10:45 IC3-Guided Abstraction (Slides)
Alexander Ivrii, Arie Matsliah, Hari Mony and Jason Baumgartner
10:45-11:15 Coffee break

Session 8: Panel Session. Model Checking in the Cloud
Chair: Maher Mneimneh, Atrenta Slides

Armin Biere, JKU Slides
Daryl Stewart, ARM Slides
Olivier Coudert, Sicad Slides
Sven Beyer, OneSpin Solutions Slides
Vigyan Singhal, Oski Technology Slides

12:15-13:30 Lunch

Invited talk from ARM by Daryl Stewart. Abstract Slides
Formal for Everyone - Challenges in Achievable Multicore Design and Verification
Chair: Youssef Hamadi, Microsoft Research Cambridge, UK

  Session 9: Solver Applications
Chair: Bruno Dutertre, SRI, USA
14:15-14:45 A quantifier-free SMT encoding of non-linear hybrid automata
Alessandro Cimatti, Sergio Mover and Stefano Tonetta
Best Paper Award

Piecewise Linear Modeling of Nonlinear Devices for Formal Verification of Analog Circuits
Yan Zhang, Sriram Sankaranarayanan and Fabio Somenzi

15:15-15:30 Forward and Backward: Bounded Model Checking of Linear Hybrid Automata From Two Directions
Yang Yang, Lei Bu and Xuandong Li
15:30-16:00 Closing