| 2017 | Checkable Proofs for First-Order Theorem Proving. | Giles Reger, Martin Suda |
| 2017 | Formal Verification of Financial Algorithms. | Grant Olney Passmore, Denis Ignatovich |
| 2017 | WorkflowFM: A Logic-Based Framework for Formal Process Specification and Composition. | Petros Papapanagiotou, Jacques D. Fleuriot |
| 2017 | CSI: New Evidence - A Progress Report. | Julian Nagele, Bertram Felgenhauer, Aart Middeldorp |
| 2017 | A Proof Strategy Language and Proof Script Generation for Isabelle/HOL. | Yutaka Nagashima, Ramana Kumar |
| 2017 | Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions. | J Strother Moore, Marijn J. H. Heule |
| 2017 | Relational Constraint Solving in SMT. | Baoluo Meng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett |
| 2017 | DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL. | Florian Lonsing, Uwe Egly |
| 2017 | Efficient Verified (UN)SAT Certificate Checking. | Peter Lammich |
| 2017 | A Unifying Principle for Clause Elimination in First-Order Logic. | Benjamin Kiesl, Martin Suda |
| 2017 | Scavenger 0.1: A Theorem Prover Based on Conflict Resolution. | Daniyar Itegulov, John K. Slaney, Bruno Woltzenlogel Paleo |
| 2017 | Theorem Proving for Metric Temporal Logic over the Naturals. | Ullrich Hustadt, Ana Ozaki, Clare Dixon |
| 2017 | On the Combination of the Bernays-Schnfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic. | Matthias Horbach, Marco Voigt, Christoph Weidenbach |
| 2017 | Short Proofs Without New Variables. | Marijn J. H. Heule, Benjamin Kiesl, Armin Biere |
| 2017 | The Potential of Interference-Based Proof Systems. | Marijn Heule, Benjamin Kiesl |
| 2017 | 24 Challenges in Deductive Software Verification. | Reiner Hhnle, Marieke Huisman |
| 2017 | A Case for Query-driven Predicate Answer Set Programming. | Gopal Gupta, Elmer Salazar, Kyle Marple, Zhuo Chen, Farhad Shakerin |
| 2017 | Splitting Proofs for Interpolation. | Bernhard Gleiss, Laura Kovcs, Martin Suda |
| 2017 | Beyond DRAT: Challenges in Certifying UNSAT. | Bertram Felgenhauer |
| 2017 | Monte Carlo Tableau Proof Search. | Michael Frber, Cezary Kaliszyk, Josef Urban |
| 2017 | Notions of Knowledge in Combinations of Theories Sharing Constructors. | Serdar Erbatur, Andrew M. Marshall, Christophe Ringeissen |
| 2017 | The Binomial Pricing Model in Finance: A Formalization in Isabelle. | Mnacho Echenim, Nicolas Peltier |
| 2017 | Efficient Certified RAT Verification. | Lus Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann, Peter Schneider-Kamp |
| 2017 | Making Automatic Theorem Provers more Versatile. | Simon Cruanes |
| 2017 | Satisfiability Modulo Bounded Checking. | Simon Cruanes |