Proceedings of Formal Methods in Computer-Aided Design, FMCAD 2015
Access full-text files
Date
2015-09
Authors
Formal Methods in Computer Aided Design
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
Department
Description
Table of Contents: Proving Hybrid Systems / by Andre Platzer (p.1) -- Formal Verification of Arithmetic Datapaths using Algebraic Geometry and Symbolic Computation / by Priyank Kalla (p.2) -- Reactive Synthesis / by Roderick Bloem (p.3) -- Abductive Inference and Its Applications in Program Analysis, Verification, and Synthesis / by Isil Diling (p.4) -- Democratization of Formal Verification with Collective Intelligence / Ziyad Hanna (p.5) -- Detecting Hardware Trojans: A Tale of Two Techniques / by Sharad Malik (p.6) --The Genesis and Development of Model Checking: Fact vs. Fiction / by Allen Emerson (p.7) -- The FMCAD 2015 Graduate Student Forum / by Georg Weissenbacher (p.8) -- Verification of Cache Coherence Protocols wrt. Trace Filters / by Parosh Aziz Abdulla, Mohamed Faouzi Atig, Zeinab Ganjei, Ahmed Rezine and Yunyun Zhu (p.9) -- Compositional Reasoning Gotchas in Practice / by Chirag Agarwal, Paul Hylander, Yogesh Mahajan, Jonathan Michelson and Vigyan Singhal (p.17) -- Universal Boolean Functional Vectors / by Jesse Bingham (p.25) -- Compositional Safety Verification with Max-SMT / by Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodr´ıguez Carbonell and Albert Rubio (p.33) --Formal Verification of Automatic Circuit Transformations for Fault-Tolerance by / Dmitry Burlyaev and Pascal Fradet (p.41) -- An SMT-based Approach to Fair Termination Analysis / by Javier Esparza and Philipp J. Meyer (p.49) -- Compositional Recurrence Analysis / by Azadeh Farzan and Zachary Kincaid (p.57) -- Pushing to the Top / by Arie Gurfinkel and Alexander Ivrii (p.65) -- Skolem Functions for Factored Formulas / by Ajith John, Shetal Shah, Supratik Chakraborty, Ashutosh Trivedi and S. Akshay (p.73) -- Theory-Aided Model Checking of Concurrent Transition Systems / by Guy Katz, Clark Barrett and David Harel (p.81) -- Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays / by Anvesh Komuravelli, Nikolaj Bjorner, Arie Gurfinkel and Kenneth McMillan (p.89) -- IC3 Software Model Checking on Control Flow Automata / by Tim Lange, Martin R. Neuhaußer and Thomas Noll (p.97) -- Accelerating Invariant Generation / by Kumar Madhukar, Bjorn Wachter, Daniel Kroening, Matt Lewis and Mandayam Srivas (p.105) -- Comparing Different Functional Allocations in Automated Air Traffic Control Design / by Cristian Mattarei, Alessandro Cimatti, Marco Gario, Stefano Tonetta and Kristin Y. Rozier (p.112) -- Pattern-based Synthesis of Synchronization for the C++ Memory Model / by Yuri Meshman, Noam Rinetzky and Eran Yahav (p.120) -- Better Lemmas with Lambda Extraction / by Mathias Preiner, Aina Niemetz and Armin Biere (p.128) -- CAQE: A Certifying QBF Solve / by Markus N. Rabe and Leander Tentrup (p.136) -- Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs. / by Moritz Sinn, Florian Zuleger and Helmut Veith (p. 144) -- Reverse Engineering with Simulation Graphs / by Mathias Soeken, Baruch Sterin, Rolf Drechsler and Robert Brayton (p.152) -- Template-based Synthesis of Instruction-Level Abstractions for SoC Verification / by Pramod Subramanyan, Yakir Vizel, Sayak Ray and Sharad Malik (p.160) -- Transaction Flows and Executable Models: Formalization and Analysis of Message passing Protocols / by Murali Talupur, Sandip Ray and John Erickson (p.168)