| 2017 | Formalization of some central theorems in combinatorics of finite sets. | Abhishek Kr Singh |
| 2017 | Reasoning with Concept Diagrams about Antipatterns. | Zohreh Shams, Mateja Jamnik, Gem Stapleton, Yuri Sato |
| 2017 | Translating C# to Branching Symbolic Transducers. | Olli Saarikivi, Margus Veanes |
| 2017 | Set of Support for Theory Reasoning. | Giles Reger, Martin Suda |
| 2017 | Towards a Semantics of Unsatisfiability Proofs with Inprocessing. | Tobias Philipp, Adrin Rebola-Pardo |
| 2017 | Synchronizing Constrained Horn Clauses. | Dmitry Mordvinov, Grigory Fedyukovich |
| 2017 | Deep Network Guided Proof Search. | Sarah M. Loos, Geoffrey Irving, Christian Szegedy, Cezary Kaliszyk |
| 2017 | Quantified Boolean Formulas: Call the Plumber! | Josef Lindsberger, Alexander Maringele, Georg Moser |
| 2017 | A uniform framework for substructural logics with modalities. | Bjrn Lellmann, Carlos Olarte, Elaine Pimentel |
| 2017 | First-Order Interpolation and Interpolating Proof Systems. | Laura Kovcs, Andrei Voronkov |
| 2017 | Blocked Clauses in First-Order Logic. | Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, Armin Biere |
| 2017 | Quantified Heap Invariants for Object-Oriented Programs. | Temesghen Kahsai, Rody Kersten, Philipp Rmmer, Martin Schf |
| 2017 | Deep Proof Search in MELL. | Ozan Kahramanogullari |
| 2017 | Coq without Type Casts: A Complete Proof of Coq Modulo Theory. | Jean-Pierre Jouannaud, Pierre-Yves Strub |
| 2017 | Cauliflower: a Solver Generator for Context-Free Language Reachability. | Nicholas Hollingum, Bernhard Scholz |
| 2017 | Towards an Abstraction-Refinement Framework for Reasoning with Large Theories. | Julio Csar Lpez-Hernndez, Konstantin Korovin |
| 2017 | On the Interaction of Inclusion Dependencies with Independence Atoms. | Miika Hannula, Juha Kontinen, Sebastian Link |
| 2017 | Higher order interpretation for higher order complexity. | Emmanuel Hainry, Romain Pchoux |
| 2017 | Theorem Provers For Every Normal Modal Logic. | Tobias Gleiner, Alexander Steen, Christoph Benzmller |
| 2017 | A One-Pass Tree-Shaped Tableau for LTL+Past. | Nicola Gigante, Angelo Montanari, Mark Reynolds |
| 2017 | TacticToe: Learning to Reason with HOL4 Tactics. | Thibault Gauthier, Cezary Kaliszyk, Josef Urban |
| 2017 | Analyzing Runtime Complexity via Innermost Runtime Complexity. | Florian Frohn, Jrgen Giesl |
| 2017 | Programming by Composing Filters. | Jeffrey Fischer, Rupak Majumdar |
| 2017 | RACCOON: A Connection Reasoner for the Description Logic ALC. | Dimas Melo Filho, Fred Freitas, Jens Otten |
| 2017 | Parallel Graph Rewriting with Overlapping Rules. | Rachid Echahed, Aude Maignan |