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