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

Accepted Papers for FMCAD 2013

Authors
Paper
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith and Josef Widder Parameterized Model Checking of Fault-tolerant Distributed Algorithms by Abstraction
Alexander Nadel, Vadim Ryvchin and Ofer Strichman Efficient MUS Extraction with Resolution
Daniel Larraz, Albert Oliveras, Enric Rodríguez Carbonell and Albert Rubio Proving Termination of Imperative Programs Using Max-SMT
Krishnendu Chatterjee, Thomas Henzinger, Jan Otop and Andreas Pavlogiannis Distributed Synthesis for LTL Fragments
Gadi Aleksandrowisz, Jason Baumgartner, Alexander Ivrii and Ziv Nevo Generalized Counter-Examples to Liveness Properties
Marijn Heule, Warren Hunt and Nathan Wetzler Trimming while Checking Clausal Proofs
Eugene Goldberg and Panagiotis Manolios Quantifier Elimination via Clause Redundancy
Sicun Gao, Soonho Kong and Edmund Clarke Satisfiability Modulo ODEs
Yifei Yuan, Anduo Wang, Rajeev Alur and Boon Loo On the Feasibility of Automation for Bandwidth Allocation Problems in Data Centers
Jijie Wei, Mark Greenstreet, Yan Peng and Ge Yu Verifying Global Convergence for a Digital Phase-Locked Loop
Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout and Fatiha Zaidi Invariants for Finite Instances and Beyond
Alex Horn, Michael Tautschnig, Celina Val, Lihao Liang, Tom Melham, Jim Grundy and Daniel Kroening Formal Co-Validation of Low-Level Hardware/Software Interfaces
Viktor Kuncak and Régis Blanc Interpolation for Synthesis on Unbounded Domains
Georg Hofferek, Ashutosh Gupta, Bettina Könighofer, Jie-Hong Roland Jiang and Roderick Bloem Synthesizing Multiple Boolean Functions using Interpolation on a Single Proof
David Deharbe, Pascal Fontaine, Daniel Le Berre and Bertrand Mazure Computing prime implicants
Rajeev Alur, Salar Moarref and Ufuk Topcu Counter-Strategy Guided Refinement of GR(1) Temporal Logic Specifications
Yulia Demyanova, Helmut Veith and Florian Zuleger On the Concept of Variable Roles and its Use in Software Analysis (Short Paper)
Sagar Chaki, Arie Gurfinkel and Ofer Strichman Verifying Periodic Programs with Priority Inheritance Locks
Hassan Eldib and Chao Wang An SMT Based Method for Optimizing Arithmetic Computations in Embedded Software Code
Philipp Ruemmer and Pavle Subotic Exploring Interpolants
Dejan Jovanović, Clark Barrett and Leonardo De Moura The Design and Implementation of the Model Constructing Satisfiability Calculus
Timothy King, Clark Barrett and Bruno Dutertre Sum of Infeasibility Simplex for SMT
Divjyot Sethi, Srinivas Narayana and Sharad Malik Abstractions for Model Checking SDN Controllers
John O'Leary, Roope Kaivola and Tom Melham Relational STE and Theorem Proving for Formal Verification of Industrial Circuit Designs
Saqib Sohail and Fabio Somenzi Efficient Handling of Obligation Constraints in Synthesis from Omega-Regular Specifications
Zyad Hassan, Aaron Bradley and Fabio Somenzi Better Generalization in IC3
Sam Bayless, Celina Val, Thomas Ball, Holger Hoos and Alan Hu Efficient Modular SAT Solving for IC3
Alessandro Cimatti, Alberto Griggio, Sergio Mover and Stefano Tonetta Parameter Synthesis with IC3
Niklas Een, Baruch Sterin and Koen Claessen A Circuit Approach to LTL Model Checking
Björn Wachter, Daniel Kroening, and Joel Ouaknine Verifying Multithreaded Software with Impact