| 2014 | Post-silicon timing diagnosis made simple using formal technology. | Daher Kaiss, Jonathan Kalechstain |
| 2014 | On interpolants and variable assignments. | Pavel Janck, Jan Kofron, Simone Fulvio Rollini, Natasha Sharygina |
| 2014 | Small inductive safe invariants. | Alexander Ivrii, Arie Gurfinkel, Anton Belov |
| 2014 | Efficient extraction of Skolem functions from QRAT proofs. | Marijn Heule, Martina Seidl, Armin Biere |
| 2014 | Computer-aided verification technology for biology. | Thomas A. Henzinger |
| 2014 | Challenging problems in industrial formal verification. | Ziyad Hanna |
| 2014 | DRUPing for interpolates. | Arie Gurfinkel, Yakir Vizel |
| 2014 | Simulation and formal verification of x86 machine-code programs that make system calls. | Shilpi Goel, Warren A. Hunt Jr., Matt Kaufmann, Soumava Ghosh |
| 2014 | Template-based circuit understanding. | Adri Gascn, Pramod Subramanyan, Bruno Dutertre, Ashish Tiwari, Dejan Jovanovic, Sharad Malik |
| 2014 | A tour of CVC4: How it works, and how to use it. | Morgan Deters, Andrew Reynolds, Tim King, Clark W. Barrett, Cesare Tinelli |
| 2014 | Faster temporal reasoning for infinite-state programs. | Byron Cook, Heidy Khlaaf, Nir Piterman |
| 2014 | Disproving termination with overapproximation. | Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn |
| 2014 | Efficient verification of periodic programs using sequential consistency and snapshots. | Sagar Chaki, Arie Gurfinkel, Nishant Sinha |
| 2014 | Interpolation with Guided Refinement: Revisiting incrementality in SAT-based unbounded model checking. | Gianpiero Cabodi, Marco Palena, Paolo Pasini |
| 2014 | Synthesis of synchronization using uninterpreted functions. | Roderick Bloem, Georg Hofferek, Bettina Knighofer, Robert Knighofer, Simon Ausserlechner, Raphael Spork |
| 2014 | SAT-based methods for circuit synthesis. | Roderick Bloem, Uwe Egly, Patrick Klampfl, Robert Knighofer, Florian Lonsing |
| 2014 | Towards Pareto-optimal parameter synthesis for monotonic cost functions. | Benjamin Bittner, Marco Bozzano, Alessandro Cimatti, Marco Gario, Alberto Griggio |
| 2014 | Response property checking via distributed state space exploration. | Brad D. Bingham, Mark R. Greenstreet |
| 2014 | Challenges in bit-precise reasoning. | Armin Biere |
| 2014 | Leveraging linear and mixed integer programming for SMT. | Tim King, Clark W. Barrett, Cesare Tinelli |
| 2013 | On the feasibility of automation for bandwidth allocation problems in data centers. | Yifei Yuan, Anduo Wang, Rajeev Alur, Boon Thau Loo |
| 2013 | Verifying global convergence for a digital phase-locked loop. | Jijie Wei, Yan Peng, Ge Yu, Mark R. Greenstreet |
| 2013 | The FMCAD graduate student forum. | Thomas Wahl |
| 2013 | Verifying multi-threaded software with impact. | Bjrn Wachter, Daniel Kroening, Jol Ouaknine |
| 2013 | Efficient handling of obligation constraints in synthesis from omega-regular specifications. | Saqib Sohail, Fabio Somenzi |