| 2020 | Give Reasoning a Trie. | Thomas Prokosch, Franois Bry |
| 2020 | Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs. | Clment Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross, Adam Chlipala |
| 2020 | Efficient Automated Reasoning About Sets and Multisets with Cardinality Constraints. | Ruzica Piskac |
| 2020 | A Programmer's Text Editor for a Logical Theory: The SUMOjEdit Editor (System Description). | Adam Pease |
| 2020 | The Imandra Automated Reasoning System (System Description). | Grant O. Passmore, Simon Cruanes, Denis Ignatovich, Dave Aitken, Matt Bray, Elijah Kagan, Kostya Kanishev, Ewen Maclean, Nicola Mometto |
| 2020 | Equality Preprocessing in Connection Calculi. | Benjamin E. Oliver, Jens Otten |
| 2020 | Deep Generation of Coq Lemma Names Using Elaborated Terms. | Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric |
| 2020 | Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation. | Filip Maric |
| 2020 | Computing Tropical Prevarieties With Satisfiability Modulo Theories (SMT) Solvers. | Christoph Lders |
| 2020 | Evaluation of Axiom Selection Techniques. | Qinghua Liu, Zishi Wu, Zihao Wang, Geoff Sutcliffe |
| 2020 | Simplifying Casts and Coercions (Extended Abstract). | Robert Y. Lewis, Paul-Nicolas Madelaine |
| 2020 | A Fast Verified Liveness Analysis in SSA Form. | Jean-Christophe Lchenet, Sandrine Blazy, David Pichardie |
| 2020 | Deciding Simple Infinity Axiom Sets with One Binary Relation by Means of Superpostulates. | Timm Lampert, Anderson Nakano |
| 2020 | Efficient Verified Implementation of Introsort and Pdqsort. | Peter Lammich |
| 2020 | Logic-Independent Proof Search in Logical Frameworks - (Short Paper). | Michael Kohlhase, Florian Rabe, Claudio Sacerdoti Coen, Jan Frederik Schaefer |
| 2020 | Trakhtenbrot's Theorem in Coq - A Constructive Approach to Finite Model Theory. | Dominik Kirst, Dominique Larchey-Wendling |
| 2020 | Soft Subexponentials and Multiplexing. | Max I. Kanovich, Stepan L. Kuznetsov, Vivek Nigam, Andre Scedrov |
| 2020 | ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description). | Jan Jakubuv, Karel Chvalovsk, Miroslav Olsk, Bartosz Piotrowski, Martin Suda, Josef Urban |
| 2020 | Formal Proof of the Group Law for Edwards Elliptic Curves. | Thomas C. Hales, Rodrigo Raya |
| 2020 | Monadic Decomposition in Integer Linear Arithmetic. | Matthew Hague, Anthony W. Lin, Philipp Rmmer, Zhilin Wu |
| 2020 | Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL. | Walter Guttmann |
| 2020 | mu-term: Verify Termination Properties Automatically (System Description). | Ral Gutirrez, Salvador Lucas |
| 2020 | Automatically Proving and Disproving Feasibility Conditions. | Ral Gutirrez, Salvador Lucas |
| 2020 | Formalization of Forcing in Isabelle/ZF. | Emmanuel Gunther, Miguel Pagano, Pedro Snchez Terraf |
| 2020 | Solving Bitvectors with MCSAT: Explanations from Bits and Pieces. | Stphane Graham-Lengrand, Dejan Jovanovic, Bruno Dutertre |