Download the entire proceedings.
The slides from sessions 5a, and 7a are still unavailable (and the associated links are broken). These links will work as the slides come in. If any other slides are missing, feel free to contact ragerdl@cs.utexas.edu.
| Sunday 10/30 | Tutorial Day |
| 8:00 | Registration/breakfast |
| 8:45-9:00 | Welcome |
| 9:00-10:30 |
John Hughes,
Professor at Chalmers University of Technology and CEO of
QuviQ: Specification Based Testing with QuickCheck Slides |
| 10:30-11:00 | Coffee break |
| 11:00-12:30 | Ivan
Sutherland, Visiting Scientist at Portland State University, ACM
Turing Award winner (1988), member of National Academy of Engineering
and National Academy of Sciences: Self-Timing: a Step Beyond Synchrony Slides |
| 12:30-14:00 | Lunch in the Tejas Dining Room (lunch is included with registration) |
| 14:00-15:00 | Fabio Somenzi,
Professor at CU Boulder: IC3: Where Monolithic and Incremental Meet Slides |
| 15:00-16:00 | Vigyan
Singhal, President and CEO of Oski Technology Inc:
End-to-End Formal using Abstractions to Maximize Coverage Slides |
| 16:00-16:30 | Coffee break |
| 16:30-18:00 | Aarti Gupta,
Senior Researcher at NEC: Verifying Concurrent Programs Slides |
| Monday 10/31 | Session Day 1 |
| 8:00 | Registration/breakfast |
| 9:00-10:00 |
Keynote J
Moore, winner of the ACM System Award (2005), member of
National Academy of Engineering, and ACM Fellow: The Role of Human Creativity in Mechanized Verification Slides |
| 10:00-10:30 | Coffee break |
| Session 1: SAT and SMT advances Chair: Karem Sakallah |
|
| 10:30-11:00 | Kenneth Mcmillan: Interpolants from Z3 proofs Slides |
| 11:00-11:30 |
Alberto Griggio:
Effective word-level interpolation for software verification Slides |
| 11:30-11:45 |
Anton Belov
and Joao
Marques-Silva: Accelerating MUS extraction with recursive model rotation Slides |
| 11:45-12:00 |
Panagiotis
Manolios
and Vasilis
Papavasileiou: Pseudo-Boolean solving by incremental translation to SAT Slides |
| 12:00-13:30 | Lunch in the Tejas Dining Room (lunch is included with registration) |
| Session 2: Application of solvers Chair: Armin Biere |
|
| 13:30-14:00 |
Harsh Raju
and Panagiotis
Manolios: Automated specification analysis using an interactive theorem prover Slides |
| 14:00-14:30 | Alessandro
Cimatti, Sergio
Mover,
and Stefano
Tonetta: Proving and explaining the unfeasibility of message sequence charts for hybrid systems Slides |
| 14:30-14:45 | Charlie Shucheng Zhu, Georg Weissenbacher and Sharad
Malik: Post-silicon fault localization using maximum satisfiability and backbones Slides |
| 14:45-15:00 | Mohamed Basith, Tariq Ahmed, Andre Rossi and Maciej
Ciesielski: Algebraic approach to arithmetic design verification Slides |
| 15:00-15:30 | Coffee break |
| Session 3: Formal verification of programs Chair: Natasha Sharyghina |
|
| 15:30-16:00 | Sagar
Chaki, Arie
Gurfinkel
and Ofer
Strichman: Time-bounded analysis of real-time systems Slides |
| 16:00-16:30 | Jonathan Kotker, Dorsa Sadigh and Sanjit
Seshia: Timing analysis of interrupt-driven programs under context bounds Slides |
| 16:30-17:00 | Robert
Koeninghofer
and Roderick
Bloem: Automated error localization and correction for imperative programs Slides |
| 17:00 | Business Meeting |
| Evening | Halloween on 6th street (organize amongst ye selves) -- The main bar area is between Neches and Brazos. A fun 70s and 80s dance bar is Barbarella. |
| Tuesday 11/1 | Session Day 2 |
| 8:00-9:00 | Breakfast |
| 8:30 | Registration |
| Session 4: Advances in equivalence- and property-checking technology Chair: Jeremy Levitt |
|
| 9:00-9:30 | Michael Case, Jason
Baumgartner, Hari Mony and Robert
Kanzelman: Optimal redundancy removal without fixedpoint computation Slides |
| 9:30-10:00 | Bryan
Brady, Randy
Bryant
and Snajit
Seshia: Learning conditional abstractions Slides |
| 10:00-10:30 | Michael Case, Jason Baumgartner, Hari Mony and Robert
Kanzelman: Approximate reachability with combined symbolic and ternary simulation Slides |
| 10:30-11:00 | Coffee break |
| Session 5: IC3 - advancements and applications Chair: Gianpierro Cobodi |
|
| 11:00-11:30 | Niklas Een, Alan Mishchenko
and Robert Brayton: Efficient implementation of property-directed reachability No slides provided |
| 11:30-12:00 | Hana Chokler, Alexander Ivrii, Arie Matsliah, Shiri Moran and
Ziv Nevo: Incremenatal formal verification of hardware Slides |
| 12:00-12:30 | Aaron Bradley, Fabio Somenzi, Zyad Hassan and Yan
Zhang: An incremental approach to model checking progress properties Slides |
| 12:30-14:00 | Lunch in the Tejas Dining Room (lunch is included with registration) |
| 14:00-15:30 | Panel: Hardware Model
Checking: Status, Challenges and Opportunities. Moderated by Murali Talupur, Intel. Panelists: Pranav Ashar (RealIntent), Jason Baumgartner (IBM), Bob Brayton (UC Berkeley), and Erick Seligman (Intel). Slides |
| 15:30-16:00 | Coffee break |
| Session 6: New formalizations and extensions Chair: Alan Hu |
|
| 16:00-16:30 | Scott Little and John
Havlicek: Realtime regular expressions for analog and mixed-signal assertions Slides |
| 16:30-17:00 | Umair Siddique
and Osman
Hasan: Formal analysis of fractional order systems in HOL Slides |
| 17:00-17:15 | Louis
Mandel, Florence
Plateau and Marc
Pouzet: Static scheduling of latency insensitive designs with Lucy-n Slides |
| 17:50-18:00 | Walk over to Judge's Hill from Conference Room |
| 18:00-22:00 | Banquet at Judge's Hill Mansion |
| Wednesday 11/2 | Session Day 3 |
| 8:00-9:00 | Breakfast |
| 8:30-9:00 | Registration |
| Session 7: Abstraction Chair: Ken McMillan |
|
| 9:00- 9:30 | Steven German: A theory of abstraction for arrays Slides |
| 9:30-10:00 | Brad Bingham, Jesse
Bingham and Mark
Greenstreet: Parametrized verification of deadlock freedom in symmetric cache coherence protocols Slides |
| 10:00-10:30 | Jayanand Asok Kumar, Lingyi Liu and Shobha
Vasudevan: Scaling probabilistic timing verification of hardware using abstractions in design source code Slides |
| 10:30-11:00 | Coffee break |
| 11:00-12:30 | Panel: Pervasive Formal Verification
in Control System Design. Moderated by Lee Pike, Galois, Inc. Panelists: Darren Cofer (Rockwell Collins), Eric Feron (Georgia Institute of Technology), Natasha Neogi (National Institute of Aerospace), Hakan Yazarel (Toyota) Slides Available for Distribution |
| 12:30-14:00 | Lunch in the Tejas Dining Room (lunch is included with registration) |
| Session 8: Micro-architecture Verification Chair: Warren A. Hunt, Jr. |
|
| 14:00-14:30 | Jun Sawada, Peter Sandon, Viresh Paruthi, Jason Baumgartner,
Michael Case and Hari Mony: Hybrid verification of a hardware modular reduction engine Slides |
| 14:30-15:00 | Sudarshan Srinivasan and Raj Katti: Desynchronization: design for verification Slides |
| 15:00-15:30 | Freek Verbeek
and Julien Schmaltz:
Hunting deadlocks efficiently in micro-architectural models of communication fabrics Slides Original, Slides PDF |
| 15:30-16:00 | Coffee break | 16:00-17:30 | Hardware Model-Checking Competition Results |
| 17:30 | Closing |