Final Program
Sunday 15. November, Tutorials and Industrial Experience Day 12:00 - 12:30 Registration 12:30 - 14:30 Tutorials (chair Armin Biere) Nikolaj Bjorner, Microsoft. Bit-Precise Constraints: Applications and Decision Procedures. Moshe Y. Vardi, Rice University. Formal Techniques for System-Level Verification. 14:30 - 15:00 Coffee 15:00 - 18:00 Industrial Experience Reports (chair Carl Pixley) Michael Theobald, D.E. Shaw. John Penix, Google. Challenges and Opportunities in Deploying Enterprise-Wide Program Analysis Tools. Joerg Bormann. Complete Functional Verification. 18:30 - 20:30 Reception Monday 16. November, 1st Conference Day 08:15 - 08:45 Registration 08:45 - 09:00 Opening (chairs Armin Biere, Carl Pixley) 09:00 - 10:30 Session 1 (chair Gianpiero Cabodi) Model Checking Yakir Vizel and Orna Grumberg. Interpolation-Sequence Based Model Checking. Alessandro Cimatti, Jori Dubrovin, Tommi Junttila and Marco Roveri. Structure-Aware Computation of Predicate Abstraction. Michael Case, Hari Mony, Jason Baumgartner and Robert Kanzelman. Enhanced Verification by Temporal Decomposition. 10:30 - 11:00 Coffee 11:00 - 12:20 Session 2 (chair Daniel Kroening) Software Verification Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu and Roberto Sebastiani. Software Model Checking via Large-Block Encoding. Jyotirmoy Deshmukh and E. Allen Emerson. Verification of Recursive Methods on Tree-like Data Structures. Subodh Sharma, Ganesh Gopalakrishnan, Eric Mercer and Jim Holt. MCC - A runtime verification tool for MCAPI user applications (short paper). 12:20 - 12:30 In Memoriam: Amir Pnueli (chair Moshe Vardi) 12:30 - 14:00 Lunch 14:00 - 15:00 Keynote (chair Armin Biere) E. Allen Emerson, University of Texas at Austin. 15:00 - 15:30 Coffee 15:30 - 17:30 Session 3 (chair Cesare Tinelli) Satisfiability Modulo Theory Leonardo de Moura and Nikolaj Bjorner. Generalized and Efficient Array Decision Procedures. Sagar Chaki, Arie Gurfinkel and Ofer Strichman. Decision Diagrams for Linear Arithmetic. Malay Ganai and Franjo Ivancic. Efficient Decision Procedure for Non-linear Arithmetic Constraints using CORDIC. Angelo Brillout, Daniel Kroening and Thomas Wahl. Mixed Abstractions for Floating-Point Arithmetic. 18:00 - 19:00 Business Meeting (chair Warren Hunt) Tuesday 17. November, 2nd Conference Day 08:30 - 09:00 Registration 09:00 - 10:00 Session 4 (chair Alessandro Cimatti) Games Saqib Sohail and Fabio Somenzi. Safety First: A Two-Stage Algorithm for LTL Games. Roderick Bloem, Karin Greimel, Thomas Henzinger and Barbara Jobstmann. Synthesizing Robust Systems. 10:00 - 10:30 Coffee 10:30 - 11:30 Session 5 (chair Alan Hu) Quantitative Reasoning William Denman, Behzad Akbarpour, Sofiene Tahar, Mohamed H. Zaki and Lawrence Paulson. Automated Formal Verification of Analog Designs using MetiTarski. Krishnan Kailas, Viresh Paruthi and Brian Monwai. Formal Verification of Correctness and Performance of Random Priority-based Arbiters. 11:30 - 12:20 Session 6 (chair Natasha Sharygina) Assume Guarantee Reasoning Zurab Khasidashvili, Gavriel Gavrielov and Tom Melham. Assume-Guarantee Validation for STE Properties within an SVA Environment. He Zhu, Fei He, William N.N. Hung, Xiaoyu Song and Ming Gu. Data Mining based Decomposition for Assume-Guarantee Reasoning (short paper). 12:20 - 14:00 Lunch 14:00 - 15:30 Session 7 (chair Koen Claessen) Equivalence Checking Jason Baumgartner, Hari Mony, Michael Case, Jun Sawada and Karen Yorav. Scalable Conditional Equivalence Checking: An Automated Invariant-Generation Based Approach. Zurab Khasidashvili, Mahmoud Kinanah and Andrei Voronkov. Verifying Equivalence of Memories Using a First Order Logic Theorem Prover. Zurab Khasidashvili, Daher Kaiss and Doron Bustan. A Compositional Theory for Observational Equivalence Checking of Hardware. 15:30 - 16:00 Coffee 16:00 - 17:30 Semiconductor Panel Panelists Ken Albin, AMD. Alan Carlin, Freescale. Velu Durairaj, TI. Alan Hunter, ARM. Tushar Ringe, Analog Devices. Dan Smith, NVIDIA. Moderator Adnan Aziz, University of Texas at Austin. 19:00 - 22:00 Conference Dinner Wednesday 18. November, 3rd and Last Conference Day 08:30 - 09:00 Registration 09:00 - 10:00 Keynote (chair Carl Pixley) John D. Barton, Intel. 10:00 - 10:30 Coffee 10:30 - 11:50 Session 8 (chair Mukul Prasad) Debugging Brian Keng and Andreas Veneris. Scaling VLSI Design Debugging with Interpolation. Robert Koenighofer, Georg Hofferek and Roderick Bloem. Debugging Formal Specifications Using Simple Counterstrategies. Sandip Ray and Warren Hunt. Connecting Pre-silicon and Post-silicon Verification (short paper). 11:50 - 14:00 EDA Vendors Lunch Panel Panelists Harry Foster, Mentor. Ziyad Hanna, Jasper. Kevin Harrer, Synopsys. Axel Scherer, Cadence. Moderator JL Gray, Verilab. 14:00 - 16:00 Session 9 (chair Anna Slobodova) Case Studies and Verification in the Large Sergey Tverdyshev. A Verified Platform for a Gate-Level Electronic Control Unit. John O'Leary, Murali Talupur and Mark Tuttle. Protocol Verification using Flows: An Industrial Experience. Jesse Bingham, Flemming Andersen, John Erickson and Gaurav Singh. Industrial Strength Refinement Checking (short paper). Tom van den Broek and Julien Schmaltz. Towards a Formally Verified Network-on-Chip (short paper). Levent Erkok, Magnus Carlsson and Adam Wick. Hardware/Software Co-verification of Cryptographic Algorithms using Cryptol (short paper). 16:00 - 16:30 Coffee 16:30 - 18:00 Session 10 (chair Roderick Bloem) Synthesis Hai Zhou. Retiming and Resynthesis with Sweep are Complete for Sequential Transformations. Eli Arbel, Oleg Rokhlenko and Karen Yorav. SAT-based Synthesis of Clock Gating Functions using 3-valued Abstraction (best paper award). Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jiri Simsa, Satnam Singh and Viktor Vafeiadis. Finding Heap-Bounds for Hardware Synthesis. 18:00 - 18:15 Closing (chair Armin Biere)