Proceedings of Formal Methods in Computer Aided Design, FMCAD 2013




Formal Methods in Computer Aided Design

Journal Title

Journal ISSN

Volume Title





Table of Contents: Preface / by Barbara Jobstmann, Sandip Ray (p.iv) -- Conference Organization (p. v) – Tutorials -- Syntax-Guided Synthesis / by Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, Abhishek Udupa (p. 1) -- Network Programming in Frenetic / by Nate Foster, Arjun Guha, Mark Reitblatt, Cole Schlesinger (p. 9) -- Firmware Validation: Challenges and Opportunities / by Jim Grundy (p. 11) -- Secure Programs via Game-based Synthesis / by Somesh Jha, Tom Reps, Bill Harris (p. 12) -- Keynotes and Special Events -- Using Process Modeling and Analysis Techniques to Reduce Errors in Healthcare / by Lori A. Clarke (p. 14) -- Static Verification Based Signoff - A Key Enabler for Managing Verification Complexity in the Modern SoC / by Pranav Ashar (p. 15) -- Student Forum / by Thomas Wahl (p. 16) -- Panel / by Panagiotis Manolios (p. 17) -- Session 1: Synthesis -- Distributed Synthesis for LTL Fragments / by Krishnendu Chatterjee, Thomas Henzinger, Jan Otop and Andreas Pavlogiannis (p. 18) -- Counter-Strategy Guided Refinement of GR(1) Temporal Logic Specifications / by Rajeev Alur, Salar Moarref and Ufuk Topcu (p.26) -- Efficient Handling of Obligation Constraints in Synthesis from Omega-Regular Specifications / by Saqib Sohail and Fabio Somenzi (p. 34) -- On the Feasibility of Automation for Bandwidth Allocation Problems in Data Centers / by Yifei Yuan, Anduo Wang, Rajeev Alur and Boon Loo (p. 42) -- Session 2: Decision Procedure Enhancements -- Computing prime implicants / by David Deharbe, Pascal Fontaine, Daniel Le Berre and Bertrand Mazure (p. 46) -- A Circuit Approach to LTL Model Checking / by Niklas Een, Baruch Sterin and Koen Claessen (p. 53) -- Invariants for Finite Instances and Beyond -- Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout and Fatiha Zaidi (p. 61) -- Session 3: Interpolation, Quantifier Elimination, Synthesis-- Exploring Interpolants / by Philipp Ruemmer and Pavle Subotic (p. 69) -- Synthesizing Multiple Boolean Functions using Interpolation on a Single Proof / by Georg Hofferek, Ashutosh Gupta, Bettina Könighofer, Jie-Hong Roland Jiang and Roderick Bloem (p. 77) -- Quantifier Elimination via Clause Redundancy / by Eugene Goldberg and Panagiotis Manolios (p. 85) -- Interpolation for Synthesis on Unbounded Domains / by Viktor Kuncak and Régis Blanc (p. 93) -- Session 4: Verification of Digital, Hybrid, and Analog Systems -- Relational STE and Theorem Proving for Formal Verification of Industrial Circuit Designs / by John O'Leary, Roope Kaivola and Tom Melham (p. 97) -- Satisfiability Modulo ODEs / by Sicun Gao, Soonho Kong and Edmund Clarke (p. 105) -- Verifying Global Convergence for a Digital Phase-Locked Loop / by Jijie Wei, Mark Greenstreet, Yan Peng and Ge Yu (p. 113) -- Session 5: Embedded Software Verification --Formal Co-Validation of Low-Level Hardware/Software Interfaces / by Alex Horn, Michael Tautschnig, Celina Val, Lihao Liang, Tom Melham, Jim Grundy and Daniel Kroening (p. 121) -- An SMT Based Method for Optimizing Arithmetic Computations in Embedded Software Code / by Hassan Eldib and Chao Wang (p. 129) -- Verifying Periodic Programs with Priority Inheritance Lock / by Sagar Chaki, Arie Gurfinkel and Ofer Strichman (p. 137) --Abstractions for Model Checking SDN Controllers / by Divjyot Sethi, Srinivas Narayana and Sharad Malik (p. 145) -- Session 6: IC3 and Debugging -- Efficient Modular SAT Solving for IC3 / by Sam Bayless, Celina Val, Thomas Ball, Holger Hoos and Alan Hu (p. 149) -- Better Generalization in IC3 / by Zyad Hassan, Aaron Bradley and Fabio Somenzi (p. 157) -- Parameter Synthesis with IC3 / by Alessandro Cimatti, Alberto Griggio, Sergio Mover and Stefano Tonetta (p. 165) -- Generalized Counter-Examples to Liveness Properties / by Gadi Aleksandrowicz, Jason Baumgartner, Alexander Ivrii and Ziv Nevo (p. 169) -- Session 7: SAT/SMT -- The Design and Implementation of the Model Constructing Satisfiability Calculus / by Dejan Jovanović, Clark Barrett and Leonardo De Moura (p. 173) -- Trimming while Checking Clausal Proofs / by Marijn Heule, Warren Hunt and Nathan Wetzler (p. 181) -- Sum of Infeasibility Simplex for SMT / by Timothy King, Clark Barrett and Bruno Dutertre (p. 189) -- Efficient MUS Extraction with Resolution / by Alexander Nadel, Vadim Ryvchin and Ofer Strichman (p. 197) -- Session 8: Software Verification -- Parameterized Model Checking of Fault-tolerant Distributed Algorithms by Abstraction / by Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith and Josef Widder (p. 201) -- Verifying Multithreaded Software with Impact / by Björn Wachter, Daniel Kroening and Joel Ouaknine (p. 210) -- Proving Termination of Imperative Programs Using Max-SMT / Daniel Larraz, Albert Oliveras, Enric Rodríguez Carbonell and Albert Rubio (p. 218) -- On the Concept of Variable Roles and its Use in Software Analysis (Short Paper) / by Yulia Demyanova, Helmut Veith and Florian Zuleger (p. 226) -- Author index (p. 213)
20 - 23 October, 2013 in Portland, Oregon

LCSH Subject Headings