FMCAD 2015

Program

The full proceedings of FMCAD 2015 can be found here. Individual papers can be found listed in the schedule below.

Schedule

Sunday, September 27 (Joint Tutorial with SAT and DIFTS)

See the tutorials page for more details.

The tutorial sessions will be chaired by Malay Ganai and Chao Wang.

8:00	Registration and Breakfast
9:00	Andre Platzer. Proving Hybrid Systems [Slides]
10:15	Coffee Break
10:30	Priyank Kalla. Formal Verification of Arithmetic Datapaths using Algebraic Geometry and Symbolic Computation [Slides]
11:45	Lunch
14:00	Roderick Bloem. Reactive Synthesis
15:15	Coffee Break
15:45 to 17:00	Işil Dillig. Abductive Inference and Its Application in Program Analysis, Verification, and Synthesis [Slides]
19:00	Reception: Scholz Garten (more information here).

Monday, September 28

Note: We will not be serving breakfast at the conference venue.

08:50	Welcome from the Chairs
09:00	Invited Talk: Ziyad Hanna Democratization of Formal Verification with Collective Intelligence (Session Chair: Roope Kaivola) [Slides]
10:00	Coffee Break
10:30	Session 1: Invariant Generation (Session Chair: Per Bjesse)
	Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodríguez Carbonell and Albert Rubio. Compositional Safety Verification with Max-SMT [Paper] [Slides] Kumar Madhukar, Björn Wachter, Daniel Kroening, Matt Lewis and Mandayam Srivas. Accelerating Invariant Generation [Paper] [Slides] Azadeh Farzan and Zachary Kincaid. Compositional Recurrence Analysis [Paper] [Slides]
12:00	Lunch
13:30	Student Forum (Session Chair: Georg Weissenbacher) [Paper]
15:30	Coffee Break
16:00 to 17:30	Session 2: Use of SMT Solvers & Decision Procedures (Session Chair: Anna Slobodova)
	Guy Katz, Clark Barrett and David Harel. Theory-Aided Model Checking of Concurrent Transition Systems [Paper] [Slides] Anvesh Komuravelli, Nikolaj Bjorner, Arie Gurfinkel and Kenneth McMillan. Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays [Paper] [Slides] Moritz Sinn, Florian Zuleger and Helmut Veith. Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs [Paper] [Slides]
17:45	Business Meeting (Session Chair: Warren A. Hunt, Jr.)

Tuesday, September 29

Note: We will not be serving breakfast at the conference venue.

09:00	Invited Talk: Sharad Malik Detecting Hardware Trojans: A Tale of Two Techniques. (Session Chair: Thomas Wahl) [Slides]
10:00	Coffee Break
10:30	Session 3: SAT, SMT, QBF: Development (Session Chair: Bruno Dutertre)
	Mathias Preiner, Aina Niemetz and Armin Biere. Better Lemmas with Lambda Extraction [Paper] [Slides] Ajith John, Shetal Shah, Supratik Chakraborty, Ashutosh Trivedi and S. Akshay. A CEGAR Algorithm for Generating Skolem Functions from Factored Formulas [Paper] [Slides] Leander Tentrup and Markus N. Rabe. CAQE: A Certifying QBF Solver [Paper] [Slides] Jesse Bingham. Universal Boolean Functional Vectors [Paper] [Slides]
12:30	Lunch
14:00	Session 4: (a) IC3 (b) Applications and Case Studies (Session Chair: Georg Weissenbacher)
	IC3: Arie Gurfinkel and Alexander Ivrii. Pushing to the Top [Paper] [Slides] Tim Lange, Martin R. Neuhäußer and Thomas Noll. IC3 Software Model Checking on Control Flow Automata [Paper] [Slides] Applications and Case Studies: Cristian Mattarei, Alessandro Cimatti, Marco Gario, Stefano Tonetta and Kristin Y. Rozier. Comparing Different Functional Allocations in Automated Air Traffic Control Design [Paper] [Slides] Chirag Agarwal, Paul Hylander, Yogesh Mahajan, Jonathan Michelson and Vigyan Singhal. Compositional Reasoning Gotchas in Practice [Paper] [Slides]
16:00	Coffee Break
16:30 to 18:00	Industry Panel: Formal Verification in the Industry - a 2020 vision (Session Chair: Roope Kaivola) Panelists: Per Bjesse (Synopsys) David Hardin (Rockwell Collins) Roope Kaivola (Intel) Naren Narasimhan (Calypto) Vigyan Singhal (OSKI) [Slides] Daryl Stewart (ARM)
19:30	Banquet: Green Pastures (more information here).

Wednesday, September 30

Note: We will not be serving breakfast at the conference venue.

09:00	Session 5: Concurrency and Multi-Agent Protocols (Session Chair: Daryl Stewart)
	Yuri Meshman, Noam Rinetzky and Eran Yahav. Pattern-based Synthesis of Synchronization for the C++ Memory Model [Paper] [Slides] Javier Esparza and Philipp J. Meyer. An SMT-based Approach to Fair Termination Analysis [Paper] [Slides] Parosh Aziz Abdulla, Mohamed Faouzi Atig, Zeinab Ganjei, Ahmed Rezine and Yunyun Zhu. Verification of Cache Coherence Protocols wrt. Trace Filters [Paper] [Slides] Murali Talupur, Sandip Ray and John Erickson. Transaction Flows and Executable Models: Formalization and Analysis of Message passing Protocols [Paper] [Slides]
11:00	Coffee Break
11:30	Invited Talk: Allen Emerson The Genesis and Development of Model Checking: Fact vs. Fiction (Session Chair: Thomas Wahl)
13:00	Lunch
14:30	HWMCC'15 Report: Hardware Model Checking Competition Report (Session Chair: Armin Biere)
15:00	Session 6: Circuit Verification and Synthesis (Session Chair: Armin Biere)
	Pramod Subramanyan, Yakir Vizel, Sayak Ray and Sharad Malik. Template-based Synthesis of Instruction-Level Abstractions for SoC Verification [Paper] [Slides] Mathias Soeken, Baruch Sterin, Rolf Drechsler and Robert Brayton. Reverse Engineering with Simulation Graphs [Paper] Dmitry Burlyaev and Pascal Fradet. Formal Verification of Automatic Circuit Transformations for Fault-Tolerance [Paper] [Slides]
16:30	End of Conference