FMCAD 2015
Formal Methods in Computer-Aided Design
September 27-30, 2015
Austin, Texas, USA

List of Accepted Papers for FMCAD 2015

See the student forum page for a list of accepted contributions to this year's student forum.

Guy Katz, Clark Barrett and David Harel. Theory-Aided Model Checking of Concurrent Transition Systems

Murali Talupur, Sandip Ray and John Erickson. Transaction Flows and Executable Models: Formalization and Analysis of Message passing Protocols

Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodríguez Carbonell and Albert Rubio. Compositional Safety Verification with Max-SMT

Jesse Bingham. Universal Boolean Functional Vectors

Tim Lange, Martin R. Neuhäußer and Thomas Noll. IC3 Software Model Checking on Control Flow Automata

Cristian Mattarei, Alessandro Cimatti, Marco Gario, Stefano Tonetta and Kristin Y. Rozier. Comparing Different Functional Allocations in Automated Air Traffic Control Design

Pramod Subramanyan, Yakir Vizel, Sayak Ray and Sharad Malik. Template-based Synthesis of Instruction-Level Abstractions for SoC Verification

Mathias Preiner, Aina Niemetz and Armin Biere. Better Lemmas with Lambda Extraction

Mathias Soeken, Baruch Sterin, Rolf Drechsler and Robert Brayton. Reverse Engineering with Simulation Graphs

Dmitry Burlyaev and Pascal Fradet. Formal Verification of Automatic Circuit Transformations for Fault-Tolerance

Azadeh Farzan and Zachary Kincaid. Compositional Recurrence Analysis

Yuri Meshman, Noam Rinetzky and Eran Yahav. Pattern-based Synthesis of Synchronization for the C++ Memory Model

Anvesh Komuravelli, Nikolaj Bjorner, Arie Gurfinkel and Kenneth McMillan. Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays

Arie Gurfinkel and Alexander Ivrii. Pushing to the Top

Ajith John, Shetal Shah, Supratik Chakraborty, Ashutosh Trivedi and S. Akshay. A CEGAR Algorithm for Generating Skolem Functions from Factored Formulas

Javier Esparza and Philipp J. Meyer. An SMT-based Approach to Fair Termination Analysis

Kumar Madhukar, Björn Wachter, Daniel Kroening, Matt Lewis and Mandayam Srivas. Accelerating Invariant Generation

Moritz Sinn, Florian Zuleger and Helmut Veith. Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs

Leander Tentrup and Markus N. Rabe. CAQE: A Certifying QBF Solver

Chirag Agarwal, Paul Hylander, Yogesh Mahajan, Jonathan Michelson and Vigyan Singhal. Compositional Reasoning Gotchas in Practice

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Zeinab Ganjei, Ahmed Rezine and Yunyun Zhu. Verification of Cache Coherence Protocols wrt. Trace Filters

Valid HTML 4.01 Transitional