| 2017 | A Decision Procedure for Restricted Intensional Sets. Maximiliano Cristiá, Gianfranco Rossi |
| 2017 | A Proof Strategy Language and Proof Script Generation for Isabelle/HOL. Yutaka Nagashima, Ramana Kumar |
| 2017 | A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms. Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand |
| 2017 | A Unifying Principle for Clause Elimination in First-Order Logic. Benjamin Kiesl, Martin Suda |
| 2017 | Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings Leonardo de Moura |
| 2017 | Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof. Gadi Tellez, James Brotherston |
| 2017 | Biabduction (and Related Problems) in Array Separation Logic. James Brotherston, Nikos Gorogiannis, Max I. Kanovich |
| 2017 | CSI: New Evidence - A Progress Report. Julian Nagele, Bertram Felgenhauer, Aart Middeldorp |
| 2017 | Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems. Christian Sternagel, Thomas Sternagel |
| 2017 | Certifying Safety and Termination Proofs for Integer Transition Systems. Marc Brockschmidt, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada |
| 2017 | Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints. Andreas Teucke, Christoph Weidenbach |
| 2017 | Decision Procedures for Theories of Sets with Measures. Markus Bender, Viorica Sofronie-Stokkermans |
| 2017 | DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL. Florian Lonsing, Uwe Egly |
| 2017 | Detecting Inconsistencies in Large First-Order Knowledge Bases. Stephan Schulz, Geoff Sutcliffe, Josef Urban, Adam Pease |
| 2017 | Efficient Certified RAT Verification. Luís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann, Peter Schneider-Kamp |
| 2017 | Efficient Verified (UN)SAT Certificate Checking. Peter Lammich |
| 2017 | Formal Verification of Financial Algorithms. Grant Olney Passmore, Denis Ignatovich |
| 2017 | Monte Carlo Tableau Proof Search. Michael Färber, Cezary Kaliszyk, Josef Urban |
| 2017 | Notions of Knowledge in Combinations of Theories Sharing Constructors. Serdar Erbatur, Andrew M. Marshall, Christophe Ringeissen |
| 2017 | On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic. Matthias Horbach, Marco Voigt, Christoph Weidenbach |
| 2017 | Reasoning About Concurrency in High-Assurance, High-Performance Software Systems. June Andronick |
| 2017 | Relational Constraint Solving in SMT. Baoluo Meng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett |
| 2017 | Satisfiability Modulo Bounded Checking. Simon Cruanes |
| 2017 | Satisfiability Modulo Theories and Assignments. Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar |
| 2017 | Satisfiability Modulo Transcendental Functions via Incremental Linearization. Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani |
| 2017 | Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints. Zhaowei Xu, Taolue Chen, Zhilin Wu |
| 2017 | Scalable Fine-Grained Proofs for Formula Processing. Haniel Barbosa, Jasmin Christian Blanchette, Pascal Fontaine |
| 2017 | Scavenger 0.1: A Theorem Prover Based on Conflict Resolution. Daniyar Itegulov, John K. Slaney, Bruno Woltzenlogel Paleo |
| 2017 | Short Proofs Without New Variables. Marijn J. H. Heule, Benjamin Kiesl, Armin Biere |
| 2017 | Splitting Proofs for Interpolation. Bernhard Gleiss, Laura Kovács, Martin Suda |
| 2017 | The Binomial Pricing Model in Finance: A Formalization in Isabelle. Mnacho Echenim, Nicolas Peltier |
| 2017 | Theorem Proving for Metric Temporal Logic over the Naturals. Ullrich Hustadt, Ana Ozaki, Clare Dixon |
| 2017 | Towards Logic-Based Verification of JavaScript Programs. José Fragoso Santos, Philippa Gardner, Petar Maksimovic, Daiva Naudziuniene |
| 2017 | Translating Between Implicit and Explicit Versions of Proof. Roberto Blanco, Zakaria Chihani, Dale Miller |
| 2017 | WorkflowFM: A Logic-Based Framework for Formal Process Specification and Composition. Petros Papapanagiotou, Jacques D. Fleuriot |