|
Monday, November 17 Conference, Day 1 | ||
| Tutorials Day, Chair: Anna Slobodova (Centaur Technology, USA) | ||
| 8:15-8:45 | Registration | |
| 8:45-9:00 |
Alessandro Cimatti
and Robert Jones |
Welcome and Opening Remarks [slides] |
| 9:00-10:30 | Kevin Jones (Rambus) | Analog and Mixed Signal Verification: The State of
the Art and some Open Problems
[abstract] [slides] [companion paper] |
| 10:30-11:00 | Break | |
| 11:00-12:30 | Moshe Levinger (IBM) | Building a Bridge: From Pre-Silicon Verification to
Post-Silicon Validation
[abstract] [slides] |
| 12:30-14:00 | Lunch | |
| 14:00-15:30 | Byron Cook (Microsoft Research lab @ Cambridge) | Computing bounds on space and time for hardware
compilation
[abstract] [slides] |
| 15:30-16:00 | Break | |
| 16:00-17:00 | David S. Hardin (Advanced Technology Center, Rockwell Collins, Inc.) | Considerations in the Design and Verification of
Microprocessors for Safety-Critical and Security-Critical
Applications
[abstract] [slides] |
| Panel discussion, Moderator: Alan Hu (University of British Columbia) | ||
| 17:00-18:30 | Masahiro Fujita (Univ. of Tokyo) [slides], Rajesh Gupta (Univ. of California, San Diego) [slides], Kris Konigsfeld (Intel) [slides], and Anmol Mathur (Calypto) [slides] | High Level Design and ESL: Who Cares? [slides] |
| 18:30-20:00 | Reception | |
|
Tuesday, November 18 Conference, Day 2 | ||
| 8:15-8:45 | Registration | |
| 8:45-9:00 | Opening | |
| Invited Talk , Chair: Tom Melham | ||
| 9:00-10:00 | Carl Seger (Intel) | Formal Methods and Physical Design: Match
Made in Heaven or Fools' Paradise?
[abstract] [slides] |
| 10:00-10:30 | Break | |
| Session 1: Synthesis and Verification, Chair: Koen Claessen | ||
| 10:30-11:00 | Michael Case, Alan Mishchenko, Robert Brayton, Jason Baumgartner and Hari Mony | Invariant-Strengthened Elimination of Dependent
State Elements [slides] |
| 11:00-11:30 | Jason Baumgartner, Hari Mony and Adnan Aziz. | Optimal Constraint-Preserving Netlist Simplification [slides] |
| 11:30-12:00 | Alan Mishchenko and Robert Brayton | Recording Synthesis History for Sequential Verification [slides] |
| 12:00-12:30 | Flavio M. de Paula, Marcel Gort, Alan Hu, Steve Wilton and Jin Yang. | BackSpace: Formal Analysis for Post-Silicon Debug [slides] |
| 12:30-14:00 | Lunch | |
| Session 2: Applications and Tools, Chair: Natasha Sharigina | ||
| 14:00-14:30 | Eric Smith and David Dill | Automatic Formal Verification of Block Cipher Implementations [slides] |
| 14:30-15:00 | Chao Yan and Mark Greenstreet | Verifying an Arbiter Circuit [slides] |
| 15:00-15:20 | Anna Slobodova | Formal Verification of Hardware Support For Advanced Encryption Standard (Short Paper) [slides] |
| 15:20-15:40 | Lei Bu, You Li, Linzhang Wang and Xuandong Li | BACH: Bounded Reachability Checker for Linear Hybrid Automata (Short Paper) [slides] |
| 15:40-16:00 | Break | |
| Session 3: Protocols and Parameterized verification, Chair: Lee Pike | ||
| 16:00-16:30 | Murali Talupur and Mark Tuttle | Going with the Flow: Parameterized Verification
using Message Flows [slides] |
| 16:30-17:00 | Jesse Bingham | Automatic Non-interference Lemmas for Parameterized
Model Checking [slides] |
| 17:00-17:30 | Federico Mari, Igor Melatti, Ivano Salvo, Enrico Tronci, Lorenzo Alvisi, Allen Clement and Harry Li. | Model Checking Nash Equilibria in MAD Distributed
Systems [slides] |
| 17:30-18:30 | Business meeting [slides] |
|
|
Wednesday, November 19 Conference, Day 3 | ||
| 8:15-8:45 | Registration | |
| 8:45-9:00 |
Opening
| |
| Panel discussion, Moderator: Carl Pixley (Synopsis) | ||
| 9:00-10:30 | Tom Ball (Microsoft) [slides], Ziyad Hanna (Jasper) [slides] and Moshe Vardi (Rice University) [slides] | The Future of Formal: Academic, IC, EDA, and Software Perspectives |
| 10:30-11:00 | Break | |
| Session 4: Satisfiability Modulo Theories, Chair: Roderick Bloem | ||
| 11:00-11:30 | Dan Goldwasser, Ofer Strichman and Shai Fine | A Theory-Based Decision Heuristic for DPLL(T) [slides] |
| 11:30-12:00 | Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez Carbonell and Albert Rubio | A Write-Based Solver for SAT Modulo the Theory of Arrays [slides] |
| 12:00-12:30 | George Hagen and Cesare Tinelli | Scaling up the formal verification of Lustre programs with SMT-based techniques [slides] |
| 12:30-14:00 | Lunch | |
| Session 5: Abstraction and Refinement, Chair: Pete Manolios | ||
| 14:00-14:30 | Per Bjesse | Word-Level Sequential Memory Abstraction for Model
Checking [slides] |
| 14:30-15:00 | Arie Gurfinkel and Sagar Chaki | Combining Predicate and Numeric Abstraction for
Software Model Checking [slides] |
| 15:00-15:30 | Peter Boehm and Tom Melham | A Refinement Approach to Design and Verification of
On-Chip Communication Protocols [slides] |
| 15:30-16:00 | Break | |
| Session 6: Program analysis, Chair: Ganesh Gopalakrishnan | ||
| 16:00-16:30 | Nishant Sinha | Symbolic Program Analysis using Term Rewriting and
Generalization [slides] |
| 16:30-17:00 | Magnus O. Myreen, Konrad Slind and Mike Gordon | Machine-code verification for multiple
architectures - An application of decompilation into logic [slides] |
| 17:00-17:30 | Pieter Hartel, Theo Ruys and Marc Geilen | Scheduling optimisations for SPIN to minimise
buffer requirements in synchronous data flow [slides] |
| 18:30-21:30 | Dinner Cruise | |
|
Thursday, November 20 Conference, Day 4 | ||
| 8:15-8:45 | Registration | |
| 8:45-9:00 |
Opening
| |
| Invited Talk, Chair: Mary Sheeran | ||
| 9:00-10:00 | Ken McMillan (Cadence) | Interpolation: Theory and Applications
[abstract] [slides] |
| 10:00-10:30 | Break | |
| Session 7: Requirements, Chair: Lenore Zuck | ||
| 10:30-11:00 | Deian Tabakov, Moshe Vardi, Gila Kamhi and Eli Singerman | A Temporal Language for SystemC [slides] |
| 11:00-11:30 | Hana Chockler, Arie Gurfinkel and Ofer Strichman | Beyond Vacuity: Towards the Strongest Passing Formula [slides] |
| 11:30-12:00 | Cindy Eisner and Dana Fisman | Augmenting a Regular Expression-Based Temporal Logic with Local Variables [slides] |
| 12:00-12:30 | Orna Kupferman, Wenchao Li and Sanjit A. Seshia | A Theory of Mutations with Applications to Vacuity,
Coverage, and Fault Tolerance [slides] |
| 12:30-14:00 | Lunch | |
| Session 8: Boolean and Inductive Reasoning, Chair: Wolfgang Kunz | ||
| 14:00-14:30 | Gianpiero Cabodi, Paolo Camurati, Marco Murciano, Luz Garcia, Sergio Nocco and Stefano Quer | Trading off SAT search and Variable Quantifications
for effective Unbounded Model Checking [slides] |
| 14:30-15:00 | Roopsha Samanta, Jyotirmoy Deshmukh and E Allen Emerson | Automatic Generation of Local Repairs for Boolean
Programs [slides] |
| 15:00-15:20 | Armin Biere and Robert Brummayer | Consistency Checking of All Different Constraints
over Bit-Vectors within a SAT Solver (Short Paper) [slides] |
| 15:20-15:40 | Warren Hunt, Robert Krug, Sandip Ray and Bill Young | Mechanized Information Flow Analysis through
Inductive Assertions (Short Paper) [slides] |
| 15:40-16:00 | Closing | |