Proceedings of Formal Methods in Computer-Aided Design, FMCAD 2014

Access full-text files




Formal Methods in Computer Aided Design

Journal Title

Journal ISSN

Volume Title




Table of Contents: Tutorials -- Challenging Problems in Industrial Formal Verification / by Ziyad Hanna (p. 1) -- Challenges in Bit-Precise Reasoning / by Armin Biere (p. 3) -- Efficient symbolic execution for software testing / by Johannes Kinder (p. 5) -- A Tour of CVC4: How it works, and how to use it / by Morgan Deters, Andrew Reynolds, Tim King, Clark Barrett and Cesare Tinelli (p. 7) -- Invited Talks and Student Forum -- Compiler verification for fun and profit / by Xavier Leroy (p. 9) -- Computer-Aided Verification Technology for Biology / by Thomas A. Henzinger (p. 11) -- Student Forum / by Ruzica Piskac (p. 13) -- Contributed Articles -- Response property checking via distributed state space exploration / by Brad Bingham and Mark Greenstreet (p. 15) -- Towards Pareto-Optimal Parameter Synthesis for Monotonic Cost Functions / by Benjamin Bittner, Marco Bozzano, Alessandro Cimatti, Marco Gario and Alberto Griggio (p. 23) -- SAT-Based Methods for Circuit Synthesis / by Roderick Bloem, Uwe Egly, Patrick Klamp, Robert Könighofer and Florian Lonsing (p. 31) -- Synthesis of Synchronization using Uninterpreted Functions / by Roderick Bloem, Georg Hofferek, Bettina Könighofer, Robert Könighofer, Simon Auβerlechner and Raphael Spörk (p. 35) -- Interpolation with Guided Rfinement: revisiting incrementality in SAT-based Unbounded Model Checking / by Gianpiero Cabodi, Marco Palena and Paolo Pasini (p. 43) -- Efficient Verification of Periodic Programs using Sequential Consistency and Snapshots / by Sagar Chaki, Arie Gurfinkel and Nishant Sinha (p. 51) -- Under-approximate Flowpipes for Non-linear Continuous Systems / by Xin Chen, Sriram Sankaranarayanan and Erika Abraham (p. 59) --Disproving termination with overapproximation / by Byron Cook, Carsten Fuhs, Kaustubh Nimkar and Peter O'Hearn (p. 67) -- Faster Temporal Reasoning for Infinite-State Programs / by Byron Cook, Heidy Khlaaf and Nir Piterman (p. 75) -- Template-based Circuit Understanding / by Adria Gascon, Ashish Tiwari, Bruno Dutertre, Pramod Subramanyan, Sharad Malik and Dejan Jovanovic (p. 83) -- Simulation and Formal Verification of x86 Machine-Code Programs that make System Calls / by Shilpi Goel, Warren Hunt, Matt Kaufmann and Soumava Ghosh (p. 91) -- DRUPing for Interpolants / by Arie Gurfinkel and Yakir Vizel (p. 99) -- Efficient Extraction of Skolem Functions from QRAT Proofs / by Marijn Heule, Martina Seidl and Armin Biere (p. 107) -- Small Inductive Safe Invariants / by Alexander Ivrii, Arie Gurfinkel and Anton Belov (p. 115) -- On Interpolants and Variable Assignments / by Pavel Jancik, Jan Kofron, Simone Fulvio Rollini and Natasha Sharygina (p. 123) -- Post-silicon Timing Diagnosis Made Simple using Formal Technology / by Daher Kaiss and Jonathan Kalechstain (p. 131) -- Leveraging Linear and Mixed Integer Programming for SMT / by Timothy King, Clark Barrett and Cesare Tinelli (p. 139) -- A Program Transformation for Faster Goal-Directed Search / by Akash Lal and Shaz Qadeer (p. 147) -- Infinite-State Backward Exploration of Boolean Broadcast Programs / by Peizun Liu and Thomas Wahl (p. 155) -- Kuai: A Model Checker for Software-defined Networks / by Rupak Majumdar, Sai Deep Tetali and Zilong Wang (p. 163) -- ILP Modulo Data / by Panagiotis Manolios, Vasilis Papavasileiou and Mirek Riedewald (p. 171) -- Turbo-Charging Lemmas on Demand with Don't Care Reasoning / by Aina Niemetz, Mathias Preiner and Armin Biere (p. 179) -- Reduction for Compositional Verification of Multi-Threaded Programs / by Corneliu Popeea, Andrey Rybalchenko and Andreas Wilhelm (p. 187) -- Finding Conflicting Instances of Quantified Formulas in SMT { Andrew Reynolds, Cesare Tinelli and Leonardo De Moura (p. 195) -- Using Interval Constraint Propagation for Pseudo-Boolean Constraint Solving / by Karsten Scheibler and Bernd Becker (p. 203) -- Patient-Specific Models from Inter-Patient Biological Models and Clinical Records / by Enrico Tronci, Toni Mancini, Ivano Salvo, Stefano Sinisi, Federico Mari, Igor Melatti, Annalisa Massini, Francesco Davi, Thomas Dierkes, Rainald Ehrig, Susanna Röblitz, Brigitte Leeners, Tillmann Kruger, Marcel Egli and Fabian Ille (p. 207) --Reducing CTL-live Model Checking to First-Order Logic Validity Checking / by Amirhossein Vakili and Nancy A. Day (p. 215) -- Predicate Abstraction for Reactive Synthesis { Adam Walker and Leonid Ryzhyk (p. 219) -- Author Index (p. 227)
21-24 October, 2014 in Switzerland

LCSH Subject Headings