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