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

8:00-8:45

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
11:00-13:00

Torsten Schaub, University of Potsdam
Answer Set Programming Abstract
Slides

13:00-14:00 Lunch
14:00-16:00

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

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: http://www.westminster.cam.ac.uk/. Sponsored by Microsoft Research Cambridge.
We'll walk to Westminster after the last tutorial: http://binged.it/SYRVUT.

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
9:00-10:00

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.
10:30-11:00

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

11:00-11:30

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)
18:30-20:30

Tuesday 18:30-20:30:
ARM sponsored drinks at the Castle Inn: http://thecastleinncambridge.com/
You can walk into town from MSRC: http://binged.it/SYS2zY

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
Results
17:00-19:00 Free time to travel to the banquet.
19:00-22:30 Banquet at Queens' Collegw: http://www.queens.cam.ac.uk/
You can walk to Queens' from MSRC: http://goo.gl/maps/f8jWi
Reception at 19:00, Meal at 19:30.

Thursday 25 Oct Day 3

8:00-09:00

Breakfast
Session 7: Automated Abstraction/Reduction Techniques
Chair: Mary Sheeran, Chalmers Technical University, Sweden
9:00-09:30

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
11:15-12:15

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

Panelists:
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
13:30-14:15

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
14:45-15:15

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