| 2016 | Reducing interpolant circuit size by ad-hoc logic synthesis and SAT-based weakening. | Gianpiero Cabodi, Paolo Camurati, Marco Palena, Paolo Pasini, Danilo Vendraminetto |
| 2016 | Synthesizing adaptive test strategies from temporal logic specifications. | Roderick Bloem, Robert Knighofer, Ingo Pill, Franz Rck |
| 2016 | Soundness of the quasi-synchronous abstraction. | Guillaume Baudart, Timothy Bourke, Marc Pouzet |
| 2016 | A paradigm shift in verification methodology. | Pranav Ashar |
| 2016 | SWAPPER: A framework for automatic generation of formula simplifiers based on conditional rewrite rules. | Rohit Singh, Armando Solar-Lezama |
| 2016 | Extracting behaviour from an executable instruction set model. | Brian Campbell, Ian Stark |
| 2015 | The FMCAD 2015 Graduate Student Forum. | Georg Weissenbacher |
| 2015 | Transaction Flows and Executable Models: Formalization and Analysis of Message passing Protocols. | Murali Talupur, Sandip Ray, John Erickson |
| 2015 | Template-based Synthesis of Instruction-Level Abstractions for SoC Verification. | Pramod Subramanyan, Yakir Vizel, Sayak Ray, Sharad Malik |
| 2015 | Simulation Graphs for Reverse Engineering. | Mathias Soeken, Baruch Sterin, Rolf Drechsler, Robert K. Brayton |
| 2015 | Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs. | Moritz Sinn, Florian Zuleger, Helmut Veith |
| 2015 | CAQE: A Certifying QBF Solver. | Markus N. Rabe, Leander Tentrup |
| 2015 | Better Lemmas with Lambda Extraction. | Mathias Preiner, Aina Niemetz, Armin Biere |
| 2015 | Proving Hybrid Systems. | Andr Platzer |
| 2015 | Pattern-based Synthesis of Synchronization for the C++ Memory Model. | Yuri Meshman, Noam Rinetzky, Eran Yahav |
| 2015 | Comparing Different Functional Allocations in Automated Air Traffic Control Design. | Cristian Mattarei, Alessandro Cimatti, Marco Gario, Stefano Tonetta, Kristin Y. Rozier |
| 2015 | Detecting Hardware Trojans: A Tale of Two Techniques. | Sharad Malik |
| 2015 | Accelerating Invariant Generation. | Kumar Madhukar, Bjrn Wachter, Daniel Kroening, Matt Lewis, Mandayam K. Srivas |
| 2015 | Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. | Anvesh Komuravelli, Nikolaj S. Bjrner, Arie Gurfinkel, Kenneth L. McMillan |
| 2015 | Theory-Aided Model Checking of Concurrent Transition Systems. | Guy Katz, Clark W. Barrett, David Harel |
| 2015 | Formal Verification of Arithmetic Datapaths using Algebraic Geometry and Symbolic Computation. | Priyank Kalla |
| 2015 | Skolem Functions for Factored Formulas. | Ajith K. John, Shetal Shah, Supratik Chakraborty, Ashutosh Trivedi, S. Akshay |
| 2015 | Democratization of Formal Verification with Collective Intelligence. | Ziyad Hanna |
| 2015 | Pushing to the Top. | Arie Gurfinkel, Alexander Ivrii |
| 2015 | Compositional Recurrence Analysis. | Azadeh Farzan, Zachary Kincaid |