| 2016 | Formal verification for computer security: Lessons learned and future directions. | Dawn Song |
| 2016 | Accurate ICP-based floating-point reasoning. | Karsten Scheibler, Felix Neubauer, Ahmed Mahdi, Martin Frnzle, Tino Teige, Tom Bienmller, Detlef Fehrer, Bernd Becker |
| 2016 | Equivalence checking using Grbner bases. | Amr A. R. Sayed-Ahmed, Daniel Groe, Mathias Soeken, Rolf Drechsler |
| 2016 | Trustworthy specifications of ARM v8-A and v8-M system level architecture. | Alastair Reid |
| 2016 | Integrating proxy theories and numeric model lifting for floating-point arithmetic. | Jaideep Ramachandran, Thomas Wahl |
| 2016 | Formal verification of division and square root implementations, an Oracle report. | David L. Rager, Jo C. Ebergen, Dmitry Nadezhin, Austin Lee, Cuong Kim Chau, Ben Selfridge |
| 2016 | Hybrid partial order reduction with under-approximate dynamic points-to and determinacy information. | Pavel Parzek |
| 2016 | Understanding evolution through algorithms. | Christos H. Papadimitriou |
| 2016 | Machine learning and systems for the next frontier in formal verification. | Manish Pandey |
| 2016 | A consistency checker for memory subsystem traces. | Matthew Naylor, Simon W. Moore, Alan Mujumdar |
| 2016 | Routing under constraints. | Alexander Nadel |
| 2016 | Proof certificates for SMT-based model checkers for infinite-state systems. | Alain Mebsout, Cesare Tinelli |
| 2016 | Modular specification and verification of a cache-coherent interface. | Kenneth L. McMillan |
| 2016 | Verifiable hierarchical protocols with network invariants on parametric systems. | Opeoluwa Matthews, Jesse D. Bingham, Daniel J. Sorin |
| 2016 | Lazy proofs for DPLL(T)-based SMT solvers. | Guy Katz, Clark W. Barrett, Cesare Tinelli, Andrew Reynolds, Liana Hadarean |
| 2016 | Property-directed k-induction. | Dejan Jovanovic, Bruno Dutertre |
| 2016 | On ∃ ∀ ∃! solving: A case study on automated synthesis of magic card tricks. | Susmit Jha, Vasumathi Raman, Sanjit A. Seshia |
| 2016 | Optimizing horn solvers for network repair. | Hossein Hojjat, Philipp Rmmer, Jedidiah McClurg, Pavol Cern, Nate Foster |
| 2016 | The FMCAD 2016 graduate student forum. | Hossein Hojjat |
| 2016 | Efficient uninterpreted function abstraction and refinement for word-level model checking. | Yen-Sheng Ho, Pankaj Chauhan, Pritam Roy, Alan Mishchenko, Robert K. Brayton |
| 2016 | Minimal unsatisfiable core extraction for SMT. | Ofer Guthmann, Ofer Strichman, Anna Trostanetski |
| 2016 | Equivalence checking by logic relaxation. | Eugene Goldberg |
| 2016 | Categorical semantics of digital circuits. | Dan R. Ghica, Achim Jung |
| 2016 | Verifying hyperproperties of hardware systems. | Bernd Finkbeiner, Markus N. Rabe |
| 2016 | Program synthesis for networks. | Pavol Cern |