| 2017 | Formalization of the Fundamental Group in Untyped Set Theory Using Auto2. | Bohua Zhan |
| 2017 | Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology. | Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek |
| 2017 | Verified Spilling and Translation Validation with Repair. | Julian Rosemann, Sigurd Schneider, Sebastian Hack |
| 2017 | Schulze Voting as Evidence Carrying Computation. | Dirk Pattinson, Mukesh Tiwari |
| 2017 | Effect Polymorphism in Higher-Order Logic (Proof Pearl). | Andreas Lochbihler |
| 2017 | Typing Total Recursive Functions in Coq. | Dominique Larchey-Wendling |
| 2017 | Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms. | Laureano Lambn, Francisco J. Martn-Mateos, Julio Rubio, Jos-Luis Ruiz-Reina |
| 2017 | Formally Verified Safe Vertical Maneuvers for Non-deterministic, Accelerating Aircraft Dynamics. | Yanni Kouskoulas, Daniel Genin, Aurora C. Schmidt, Jean-Baptiste Jeannin |
| 2017 | Making PVS Accessible to Generic Services by Interpretation in a Universal Format. | Michael Kohlhase, Dennis Mller, Sam Owre, Florian Rabe |
| 2017 | Categoricity Results for Second-Order ZF in Dependent Type Theory. | Dominik Kirst, Gert Smolka |
| 2017 | Automating Formalization by Statistical and Semantic Parsing of Mathematics. | Cezary Kaliszyk, Josef Urban, Jir Vyskocil |
| 2017 | Automated Theory Exploration for Interactive Theorem Proving: - An Introduction to the Hipster System. | Moa Johansson |
| 2017 | Proof Tactics for Assertions in Separation Logic. | Zhe Hou, David Sann, Alwen Tiu, Yang Liu |
| 2017 | Efficient, Verified Checking of Propositional Proofs. | Marijn Heule, Warren A. Hunt Jr., Matt Kaufmann, Nathan Wetzler |
| 2017 | Proof Certificates in PVS. | Frdric Gilbert |
| 2017 | A Formalized General Theory of Syntax with Bindings. | Lorenzo Gheri, Andrei Popescu |
| 2017 | Formalizing Basic Quaternionic Analysis. | Andrea Gabrielli, Marco Maggesi |
| 2017 | Bellerophon: Tactical Theorem Proving for Hybrid Systems. | Nathan Fulton, Stefan Mitsch, Rose Bohrer, Andr Platzer |
| 2017 | Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq. | Yannick Forster, Gert Smolka |
| 2017 | A Verified Generational Garbage Collector for CakeML. | Adam Sandberg Ericsson, Magnus O. Myreen, Johannes man Pohjola |
| 2017 | Homotopy Type Theory in Lean. | Floris van Doorn, Jakob von Raumer, Ulrik Buchholtz |
| 2017 | A Formalisation of Consistent Consequence for Boolean Equation Systems. | Myrthe van Delft, Herman Geuvers, Tim A. C. Willemse |
| 2017 | How to Get More Out of Your Oracles. | Lus Cruz-Filipe, Kim S. Larsen, Peter Schneider-Kamp |
| 2017 | A Formal Proof in Coq of LaSalle's Invariance Principle. | Cyril Cohen, Damien Rouhling |
| 2017 | FoCaLiZe and Dedukti to the Rescue for Proof Interoperability. | Raphal Cauderlier, Catherine Dubois |