FMCAD 2013
Formal Methods in Computer-Aided Design
Portland, OR, USA
October 20-23, 2013

FMCAD 2013 Program

Sunday 20 Oct Tutorial Day
Tutorial Chair: Malay Ganai

08:00-08:45

Breakfast and Registration
08:45-09:00 Welcome [Slides]
09:00-10:30 Rajeev Alur, University of Pennsylvania
Syntax-Guided Synthesis [Slides]
10:30-11:00 Coffee break
11:00-12:30 Nate Foster, Cornell University
Arjun Guha, University of Massachusetts Amherst
Mark Reitblatt, Cornell University
Cole Schlesinger, Princeton University
Network Programming in Frenetic [Slides: (PDF) (External Link)]
12:30-14:00 Lunch
14:00-15:30

Jim Grundy, Intel Corporation
Firmware Validation: Challenges and Opportunities [Slides]

15:30-16:00 Coffee break
16:00-17:30 Somesh Jha, University of Wisconsin, Madison
Tom Reps, University of Wisconsin, Madison
Bill Harris, University of Wisconsin, Madison
Secure Programs via Game-based Synthesis [Slides: (PDF) (Keynote - native format) (PPT)]
18:00-21:00 Reception at University Place Hotel, Willamette Room

Monday 21 Oct Day 1
08:00-08:45 Breakfast and Registration
08:45-09:00 Welcome and Opening Remarks [Slides]
Session 1: Synthesis
Chair: Arie Gurfinkel
09:00-09:25 (25min) Krishnendu Chatterjee, Thomas Henzinger, Jan Otop and Andreas Pavlogiannis
Distributed Synthesis for LTL Fragments [Slides]
09:25-09:50 (25min) Rajeev Alur, Salar Moarref and Ufuk Topcu
Counter-Strategy Guided Refinement of GR(1) Temporal Logic Specifications [Slides: Keynote]
09:50-10:15 (25min) Saqib Sohail and Fabio Somenzi
Efficient Handling of Obligation Constraints in Synthesis from Omega-Regular Specifications [Slides]
10:15-10:30 (15min) Yifei Yuan, Anduo Wang, Rajeev Alur and Boon Loo
On the Feasibility of Automation for Bandwidth Allocation Problems in Data Centers [Slides]
10:30-11:00 Coffee break
Session 2: Decision Procedure Enhancements
Chair: Marijn Heule
11:00-11:25 (25min) David Deharbe, Pascal Fontaine, Daniel Le Berre and Bertrand Mazure
Computing prime implicants [Slides]
11:25-11:50 (25min) Niklas Een, Baruch Sterin and Koen Claessen
A Circuit Approach to LTL Model Checking [Slides]
11:50-12:15 (25min) Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout and Fatiha Zaidi
Invariants for Finite Instances and Beyond [Slides]
12:30-14:00 Lunch
14:00-15:30
    [Schedule]
Student Forum
Chair: Thomas Wahl
15:30-16:00 Coffee Break
Session 3: Interpolation, Quantifier Elimination, Synthesis
Chair: Georg Weissenbacher
16:00-16:25 (25min) Philipp Ruemmer and Pavle Subotic
Exploring Interpolants [Slides]
16:25-16:50 (25min) Georg Hofferek, Ashutosh Gupta, Bettina Könighofer, Jie-Hong Roland Jiang and Roderick Bloem
Synthesizing Multiple Boolean Functions using Interpolation on a Single Proof [Slides]
16:50-17:15 (25min) Eugene Goldberg and Panagiotis Manolios
Quantifier Elimination via Clause Redundancy [Slides]
17:15-17:30 (15min) Viktor Kuncak and Regis Blanc
Interpolation for Synthesis on Unbounded Domains [Slides]
18:00-19:00 Business meeting [Slides]

Tuesday 22 Oct Day 2
08:00-09:00 Breakfast and Registration
09:00-10:30 Keynote: Lori A. Clarke, University of Massachusetts, Amherst
Using Process Modeling and Analysis Techniques to Reduce Errors in Healthcare
Chair: Sandip Ray
10:30-11:00 Coffee break
Session 4: Verification of Digital, Hybrid, and Analog Systems
Chair: Alan Hu
11:00-11:25 (25min) John O'Leary, Roope Kaivola and Tom Melham
Relational STE and Theorem Proving for Formal Verification of Industrial Circuit Designs [Slides]
11:25-11:50 (25min) Sicun Gao, Soonho Kong and Edmund Clarke
Satisfiability Modulo ODEs [Slides: (PDF) (External Link)]
11:50-12:15 (25min) Jijie Wei, Mark Greenstreet, Yan Peng and Ge Yu
Verifying Global Convergence for a Digital Phase-Locked Loop
12:30-14:00 Lunch
Session 5: Embedded Software Verification
Chair: Cesar Sanchez
14:00-14:25 (25min) Alex Horn, Michael Tautschnig, Celina Val, Lihao Liang, Tom Melham, Jim Grundy and Daniel Kroening
Formal Co-Validation of Low-Level Hardware/Software Interfaces [Slides]
14:25-14:50 (25min) Hassan Eldib and Chao Wang
An SMT Based Method for Optimizing Arithmetic Computations in Embedded Software Code [Slides]
14:50-15:15 (25min) Sagar Chaki, Arie Gurfinkel and Ofer Strichman
Verifying Periodic Programs with Priority Inheritance Locks [Slides: (PDF) (PPT)]
15:15-15:30 (15min) Divjyot Sethi, Srinivas Narayana and Sharad Malik
Abstractions for Model Checking SDN Controllers [Slides: (PDF) (PPT)]
15:30-16:00 Coffee break
16:00-17:00 Hardware Model Checking Competition
Chair: Armin Biere
17:00-18:00 Panel: Teaching Formal Methods: Needs, Challenges, Experiences, and Opportunities
Chair: Panagiotis Manolios
Panelists:
  • Jason Baumgartner, IBM
  • Mike Durling, GE
  • Alwyn Goodloe, NASA
  • Pete Manolios, Northeastern University
  • Vigyan Singhal, Oski
  • Moshe Vardi, Rice University
  • Helmut Veith, Vienna University of Technology
19:00-21:30 Banquet at Portland City Grill

Wednesday 23 Oct Day 3
08:00-09:00 Breakfast and Registration
09:00-10:30 Keynote: Pranav Ashar, Real Intent
Static Verification Based Signoff - A Key Enabler for Managing Verification Complexity in the Modern SoC
Chair: Warren A. Hunt, Jr.
10:30-11:00 Coffee break
Session 6: IC3 and Debugging
Chair: Philipp Ruemmer
11:00-11:25 (25min) Sam Bayless, Celina Val, Thomas Ball, Holger Hoos and Alan Hu
Efficient Modular SAT Solving for IC3 [Slides]
11:25-11:50(25min) Zyad Hassan, Aaron Bradley and Fabio Somenzi
Better Generalization in IC3 [Slides]
11:50-12:05 (15min) Alessandro Cimatti, Alberto Griggio, Sergio Mover and Stefano Tonetta
Parameter Synthesis with IC3 [Slides]
12:05-12:20 (15min) Gadi Aleksandrowisz, Jason Baumgartner, Alexander Ivrii and Ziv Nevo
Generalized Counter-Examples to Liveness Properties [Slides]
12:30-14:00 Lunch
Session 7: SAT/SMT
Chair: Alberto Griggio
14:00-14:25 (25min) Dejan Jovanovic, Clark Barrett and Leonardo De Moura
The Design and Implementation of the Model Constructing Satisfiability Calculus [Slides]
14:25-14:50 (25min) Marijn Heule, Warren Hunt and Nathan Wetzler
Trimming while Checking Clausal Proofs [Slides]
14:50-15:15 (25min) Timothy King, Clark Barrett and Bruno Dutertre
Sum of Infeasibility Simplex for SMT [Slides]
15:15-15:30 (15min) Alexander Nadel, Vadim Ryvchin and Ofer Strichman
Efficient MUS Extraction with Resolution [Slides]
15:30-16:00 Coffee break
Session 08: Software Verification
Chair: Lee Pike
16:00-16:25 (25min) Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith and Josef Widder
Parameterized Model Checking of Fault-tolerant Distributed Algorithms by Abstraction [Slides]
16:25-16:50 (25min) Daniel Kroening, Joel Ouaknine, Bjorn Watcher
Verifying Multithreaded Software with Impact [Slides]
16:50-17:15 (25min) Daniel Larraz, Albert Oliveras, Enric Rodriguez Carbonell and Albert Rubio
Proving Termination of Imperative Programs Using Max-SMT [Slides]
17:15-17:30 (15min) Yulia Demyanova, Helmut Veith and Florian Zuleger
On the Concept of Variable Roles and its Use in Software Analysis [Slides]
17:30 Closing