| 2017 | Automatic cyclic termination proofs for recursive procedures in separation logic. | Reuben N. S. Rowe, James Brotherston |
| 2017 | Verifying a hash table and its iterators in higher-order separation logic. | Franois Pottier |
| 2017 | Porting the HOL light analysis library: some lessons (invited talk). | Lawrence C. Paulson |
| 2017 | A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations. | rik Martin-Dorel, Pierre Roux |
| 2017 | Verifying dynamic race detection. | William Mansky, Yuanfeng Peng, Steve Zdancewic, Joseph Devietti |
| 2017 | Equivalence of system f and ź2 in Coq based on context morphism lemmas. | Jonas Kaiser, Tobias Tebbi, Gert Smolka |
| 2017 | BliStrTune: hierarchical invention of theorem proving strategies. | Jan Jakubuv, Josef Urban |
| 2017 | Markov processes in Isabelle/HOL. | Johannes Hlzl |
| 2017 | Formalising real numbers in homotopy type theory. | Gatan Gilbert |
| 2017 | Verified compilation of CakeML to multiple machine-code targets. | Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar |
| 2017 | Mechanized verification of preemptive OS kernels (invited talk). | Xinyu Feng |
| 2017 | A formalization of the Berlekamp-Zassenhaus factorization algorithm. | Jose Divasn, Sebastiaan J. C. Joosten, Ren Thiemann, Akihisa Yamada |
| 2017 | Lifting proof-relevant unification to higher dimensions. | Jesper Cockx, Dominique Devriese |
| 2017 | The next 700 syntactical models of type theory. | Simon Boulier, Pierre-Marie Pdrot, Nicolas Tabareau |
| 2017 | A Coq formal proof of the LaxMilgram theorem. | Sylvie Boldo, Franois Clment, Florian Faissole, Vincent Martin, Micaela Mayero |
| 2017 | Formally verified differential dynamic logic. | Rose Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Vlp, Andr Platzer |
| 2017 | The HoTT library: a formalization of homotopy type theory in Coq. | Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters |
| 2017 | Complx: a verification framework for concurrent imperative programs. | Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah, Joseph Tuong |
| 2017 | Type-and-scope safe programs and their proofs. | Guillaume Allais, James Chapman, Conor McBride, James McKinna |
| 2017 | Formal foundations of 3D geometry to model robot manipulators. | Reynald Affeldt, Cyril Cohen |
| 2016 | Planning for change in a formal verification of the raft consensus protocol. | Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, Thomas E. Anderson |
| 2016 | Formalizing jordan normal forms in Isabelle/HOL. | Ren Thiemann, Akihisa Yamada |
| 2016 | A verified algorithm for detecting conflicts in XACML access control rules. | Michel St-Martin, Amy P. Felty |
| 2016 | Axiomatic semantics for compiler verification. | Steven Schfer, Sigurd Schneider, Gert Smolka |
| 2016 | A unified Coq framework for verifying C programs with floating-point computations. | Tahina Ramananandro, Paul Mountcastle, Benot Meister, Richard Lethin |