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 |
13:00-14:00 | Lunch |
14:00-16:00 | Eric Feron, Guillaume Brat, Pierre-Loic Garoche, Pete Manolios, Marc Pantel. |
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 |
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 |
11:00-11:30 | Automatic Lock Insertion in Concurrent Programs |
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: |
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 |
|
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) |
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 Panelists: |
12:15-13:30 | Lunch |
13:30-14:15 | Invited talk from ARM by Daryl Stewart. Abstract Slides |
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 |
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 |