FMCAD 2014
Formal Methods in Computer-Aided Design
Lausanne, Switzerland
October 21-24, 2014

Proceedings

The full proceedings of FMCAD 2014 can be found here. The hyperlinks in the program below point to the individual papers.

Program

Timing Details

Location Details

The venue page is a good resource for details about the location. Some quick things to note:

Schedule

Monday 20 October
Venue: BC 420/BC 410

See DIFTS and MEMOCODE websites for details.
Tuesday, 21 October
Venue: CE 1515 (Salle Polyvalente or SPO)

Tutorials
08:00 Registration and Breakfast
Session Chair: Anna Slobodova
09:00 Ziyad Hanna: Challenging Problems in Industrial Formal Verification [Slides]
10:15 Break
Session Chair: Koen Claessen
10:30 Armin Biere: Challenges in Bit-Precise Reasoning [Slides] [Video]
11:45 Lunch
Session Chair: Darryl Stewart
13:45 Johannes Kinder: Efficient Symbolic Execution for Software Testing [Slides]
15:15 Break
Session Chair: Per Bjesse
15:45 Morgan Deters, Andrew Reynolds, Timothy King, Clark Barrett, Cesare Tinelli: A Tour of CVC4: How it works, and how to use it [Slides]
18:00 Reception in Rolex Learning Center (location)
Wednesday, 22 October
Venue: CE 1515 (Salle Polyvalente or SPO)

08:00 Registration and Breakfast
08:55 Welcome from Program Chair(s)
09:00 Welcome from James Larus, dean of the EPFL School of Computer and Communication Sciences
Session Chair: Viktor Kuncak
09:05 Invited talk by Xavier Leroy: Compiler verification for fun and profit [Slides] [Video]
10:15 Break
Session Chair: Per Bjesse
10:45 Shilpi Goel, Warren Hunt, Matt Kaufmann and Soumava Ghosh: Simulation and Formal Verification of x86 Machine-Code Programs that make System Calls [Slides]
11:15 Akash Lal and Shaz Qadeer: A Program Transformation for Faster Goal-Directed Search [Slides]
11:45 Lunch
Session Chair: Ruzica Piskac
13:30 Adam Walker and Leonid Ryzhyk. Predicate Abstraction for Reactive Synthesis [Slides]
14:00 Adria Gascon, Ashish Tiwari, Bruno Dutertre, Pramod Subramanyan, Sharad Malik and Dejan Jovanovic. Template-based Circuit Understanding [Slides]
14:30 Roderick Bloem, Georg Hofferek, Bettina Könighofer, Robert Könighofer, Simon Außerlechner and Raphael Spörk. Synthesis of Synchronization using Uninterpreted Functions [Slides]
15:00 Roderick Bloem, Uwe Egly, Patrick Klampfl, Robert Koenighofer and Florian Lonsing. SAT-Based Methods for Circuit Synthesis [Slides]
15:15 Break
Session Chair: Georg Weissenbacher
15:45 Gianpiero Cabodi, Marco Palena and Paolo Pasini. Interpolation with Guided Refinement: revisiting incrementality in SAT-based Unbounded Model Checking
16:15 Pavel Jancik, Jan Kofron, Simone Fulvio Rollini and Natasha Sharygina. On Interpolants and Variable Assignments
16:45 Yakir Vizel and Arie Gurfinkel. DRUPing for Interpolants
17:15 Business Meeting
Thursday, 23 October
Venue: CE 1515 (Salle Polyvalente or SPO)

08:00 Registration and Breakfast
Session Chair: Thomas Wahl
09:00 Rupak Majumdar, Sai Deep Tetali and Zilong Wang. Kuai. A Model Checker for Software-defined Networks
09:30 Arie Gurfinkel, Alexander Ivrii and Anton Belov. Small Inductive Safe Invariants [Slides]
10:00 Benjamin Bittner, Marco Bozzano, Alessandro Cimatti, Marco Gario and Alberto Griggio. Towards Pareto-Optimal Parameter Synthesis for Monotonic Cost Functions [Slides]
10:30 Break
Session Chair: Ruzica Piskac
10:45 Student Forum: click here to see the papers accepted to the Forum
11:45 Lunch
Session Chair: Warren A. Hunt, Jr.
13:30 Timothy King, Clark Barrett and Cesare Tinelli. Leveraging Linear and Mixed Integer Programming for SMT [Slides]
14:00 Panagiotis Manolios, Vasilis Papavasileiou and Mirek Riedewald. ILP Modulo Data [Slides]
14:30 Marijn Heule, Martina Seidl and Armin Biere. Efficient Extraction of Skolem Functions from QRAT Proofs [Slides]
15:00 Karsten Scheibler and Bernd Becker. Using Interval Constraint Propagation for Pseudo-Boolean Constraint Solving [Slides]
15:15 Break
Session Chair: Alessandro Cimatti
15:45 Andrew Reynolds, Cesare Tinelli and Leonardo De Moura. Finding Conflicting Instances of Quantified Formulas in SMT [Slides]
16:15 Aina Niemetz, Mathias Preiner and Armin Biere. Turbo-Charging Lemmas on Demand with Don't Care Reasoning [Slides]
16:45 Daher Kaiss and Jonathan Kalechstain. Post-silicon Timing Diagnosis Made Simple using Formal Technology [Slides]
17:15 End
18:30 Banquet at the Olympic Museum (location)
Friday, 24 October
Venue: CE 1515 (Salle Polyvalente or SPO)

08:00 Registration and Breakfast
Session Chair: Viktor Kuncak
09:00 Invited talk by Thomas Henzinger: Computer-Aided Verification for Biology
10:15 Break
Session Chair: Alessandro Cimatti
10:45 Xin Chen, Sriram Sankaranarayanan and Erika Abraham. Under-approximate Flowpipes for Non-linear Continuous Systems
11:15 Toni Mancini, Ivano Salvo, Federico Mari, Igor Melatti, Annalisa Massini, Stefano Sinisi, Enrico Tronci, Francesco Davi, Thomas Dierkes, Rainald Ehrig, Susanna Röblitz, Brigitte Leeners, Tillmann Kruger, Marcel Egli and Fabian Ille. Patient-Specific Models from Inter-Patient Biological Models and Clinical Records
11:45 Lunch
Session Chair: Andrey Rybalchenko
13:30 Byron Cook, Heidy Khlaaf and Nir Piterman. Faster Temporal Reasoning for Infinite-State Programs
14:00 Brad Bingham and Mark Greenstreet. Response property checking via distributed state space exploration [Slides]
14:30 Peizun Liu and Thomas Wahl. Infinite-State Backward Exploration of Boolean Broadcast Programs [Slides]
15:00 Amirhossein Vakili and Nancy A. Day. Reducing CTL-live Model Checking to First-Order Logic Validity Checking [Slides]
15:15 Break
Session Chair: Georg Weissenbacher
15:45 Byron Cook, Carsten Fuhs, Kaustubh Nimkar and Peter O'Hearn. Disproving termination with overapproximation [Slides]
16:15 Corneliu Popeea, Andrey Rybalchenko and Andreas Wilhelm. Reduction for Compositional Verification of Multi-Threaded Programs
16:45 Sagar Chaki, Arie Gurfinkel and Nishant Sinha. Efficient Verification of Periodic Programs using Sequential Consistency and Snapshots
17:15 End

Valid HTML 4.01 Transitional