Proceedings of Formal Methods in Computer Aided Design, FMCAD 2013

Date

2013

Authors

Formal Methods in Computer Aided Design

Journal Title

Journal ISSN

Volume Title

Publisher

IEEE

Abstract

Description

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

Citation