| 2016 | 2016 Formal Methods in Computer-Aided Design, FMCAD 2016, Mountain View, CA, USA, October 3-6, 2016 Ruzica Piskac, Muralidhar Talupur |
| 2016 | A consistency checker for memory subsystem traces. Matthew Naylor, Simon W. Moore, Alan Mujumdar |
| 2016 | A paradigm shift in verification methodology. Pranav Ashar |
| 2016 | Accurate ICP-based floating-point reasoning. Karsten Scheibler, Felix Neubauer, Ahmed Mahdi, Martin Fränzle, Tino Teige, Tom Bienmüller, Detlef Fehrer, Bernd Becker |
| 2016 | Categorical semantics of digital circuits. Dan R. Ghica, Achim Jung |
| 2016 | Combining requirement mining, software model checking and simulation-based verification for industrial automotive systems. Tomoya Yamaguchi, Tomoyuki Kaga, Alexandre Donzé, Sanjit A. Seshia |
| 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 | Equivalence checking by logic relaxation. Eugene Goldberg |
| 2016 | Equivalence checking using Gröbner bases. Amr A. R. Sayed-Ahmed, Daniel Große, Mathias Soeken, Rolf Drechsler |
| 2016 | Extracting behaviour from an executable instruction set model. Brian Campbell, Ian Stark |
| 2016 | Formal verification for computer security: Lessons learned and future directions. Dawn Song |
| 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 Parízek |
| 2016 | Integrating proxy theories and numeric model lifting for floating-point arithmetic. Jaideep Ramachandran, Thomas Wahl |
| 2016 | Lazy proofs for DPLL(T)-based SMT solvers. Guy Katz, Clark W. Barrett, Cesare Tinelli, Andrew Reynolds, Liana Hadarean |
| 2016 | Lazy sequentialization for TSO and PSO via shared memory abstractions. Ermenegildo Tomasco, Truc L. Nguyen, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato |
| 2016 | Machine learning and systems for the next frontier in formal verification. Manish Pandey |
| 2016 | Minimal unsatisfiable core extraction for SMT. Ofer Guthmann, Ofer Strichman, Anna Trostanetski |
| 2016 | Modular specification and verification of a cache-coherent interface. Kenneth L. McMillan |
| 2016 | Network verification - When Clarke meets Cerf. George Varghese |
| 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 Rümmer, Jedidiah McClurg, Pavol Cerný, Nate Foster |
| 2016 | Program synthesis for networks. Pavol Cerný |
| 2016 | Proof certificates for SMT-based model checkers for infinite-state systems. Alain Mebsout, Cesare Tinelli |
| 2016 | Property-directed k-induction. Dejan Jovanovic, Bruno Dutertre |
| 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 | Routing under constraints. Alexander Nadel |
| 2016 | SWAPPER: A framework for automatic generation of formula simplifiers based on conditional rewrite rules. Rohit Singh, Armando Solar-Lezama |
| 2016 | Soundness of the quasi-synchronous abstraction. Guillaume Baudart, Timothy Bourke, Marc Pouzet |
| 2016 | Synthesizing adaptive test strategies from temporal logic specifications. Roderick Bloem, Robert Könighofer, Ingo Pill, Franz Röck |
| 2016 | The FMCAD 2016 graduate student forum. Hossein Hojjat |
| 2016 | Trustworthy specifications of ARM® v8-A and v8-M system level architecture. Alastair Reid |
| 2016 | Understanding evolution through algorithms. Christos H. Papadimitriou |
| 2016 | Verifiable hierarchical protocols with network invariants on parametric systems. Opeoluwa Matthews, Jesse D. Bingham, Daniel J. Sorin |
| 2016 | Verifying hyperproperties of hardware systems. Bernd Finkbeiner, Markus N. Rabe |