FMCAD 2011
Formal Methods in Computer-Aided Design
Austin, TX, USA
October 30 - November 2

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

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
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
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
15:00-16:00 Vigyan Singhal, President and CEO of Oski Technology Inc:
End-to-End Formal using Abstractions to Maximize Coverage
16:00-16:30 Coffee break
16:30-18:00 Aarti Gupta, Senior Researcher at NEC:
Verifying Concurrent Programs

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
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
11:00-11:30 Alberto Griggio:
Effective word-level interpolation for software verification
11:30-11:45 Anton Belov and Joao Marques-Silva:
Accelerating MUS extraction with recursive model rotation
11:45-12:00 Panagiotis Manolios and Vasilis Papavasileiou:
Pseudo-Boolean solving by incremental translation to SAT
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
14:00-14:30 Alessandro Cimatti, Sergio Mover, and Stefano Tonetta:
Proving and explaining the unfeasibility of message sequence charts for hybrid systems
14:30-14:45 Charlie Shucheng Zhu, Georg Weissenbacher and Sharad Malik:
Post-silicon fault localization using maximum satisfiability and backbones
14:45-15:00 Mohamed Basith, Tariq Ahmed, Andre Rossi and Maciej Ciesielski:
Algebraic approach to arithmetic design verification
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
16:00-16:30 Jonathan Kotker, Dorsa Sadigh and Sanjit Seshia:
Timing analysis of interrupt-driven programs under context bounds
16:30-17:00 Robert Koeninghofer and Roderick Bloem:
Automated error localization and correction for imperative programs
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
9:30-10:00 Bryan Brady, Randy Bryant and Snajit Seshia:
Learning conditional abstractions
10:00-10:30 Michael Case, Jason Baumgartner, Hari Mony and Robert Kanzelman:
Approximate reachability with combined symbolic and ternary simulation
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
12:00-12:30 Aaron Bradley, Fabio Somenzi, Zyad Hassan and Yan Zhang:
An incremental approach to model checking progress properties
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).
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
16:30-17:00 Umair Siddique and Osman Hasan:
Formal analysis of fractional order systems in HOL
17:00-17:15 Louis Mandel, Florence Plateau and Marc Pouzet:
Static scheduling of latency insensitive designs with Lucy-n
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
9:30-10:00 Brad Bingham, Jesse Bingham and Mark Greenstreet:
Parametrized verification of deadlock freedom in symmetric cache coherence protocols
10:00-10:30 Jayanand Asok Kumar, Lingyi Liu and Shobha Vasudevan:
Scaling probabilistic timing verification of hardware using abstractions in design source code
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
14:30-15:00 Sudarshan Srinivasan and Raj Katti:
Desynchronization: design for verification
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
17:30 Closing

Program without sidebars.