FMCAD 2015
Formal Methods in Computer-Aided Design
September 27-30, 2015
Austin, Texas, USA


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


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
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)
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)
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)
12:30 Lunch
14:00 Session 4: (a) IC3 (b) Applications and Case Studies (Session Chair: Georg Weissenbacher)
  • 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)

  • 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)
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

Valid HTML 4.01 Transitional