| 2017 | A One-Pass Tree-Shaped Tableau for LTL+Past. Nicola Gigante, Angelo Montanari, Mark Reynolds |
| 2017 | A Quantitative Partial Model-Checking Function and Its Optimisation. Stefano Bistarelli, Fabio Martinelli, Ilaria Matteucci, Francesco Santini |
| 2017 | A uniform framework for substructural logics with modalities. Björn Lellmann, Carlos Olarte, Elaine Pimentel |
| 2017 | Analyzing Runtime Complexity via Innermost Runtime Complexity. Florian Frohn, Jürgen Giesl |
| 2017 | Automated analysis of Stateflow models. Hamza Bourbouh, Pierre-Loïc Garoche, Christophe Garion, Arie Gurfinkel, Temesghen Kahsai, Xavier Thirioux |
| 2017 | Blocked Clauses in First-Order Logic. Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, Armin Biere |
| 2017 | Bunched Hypersequent Calculi for Distributive Substructural Logics. Agata Ciabattoni, Revantha Ramanayake |
| 2017 | Cauliflower: a Solver Generator for Context-Free Language Reachability. Nicholas Hollingum, Bernhard Scholz |
| 2017 | Coq without Type Casts: A Complete Proof of Coq Modulo Theory. Jean-Pierre Jouannaud, Pierre-Yves Strub |
| 2017 | Decidable linear list constraints. Sabine Bauer, Martin Hofmann |
| 2017 | Deep Network Guided Proof Search. Sarah M. Loos, Geoffrey Irving, Christian Szegedy, Cezary Kaliszyk |
| 2017 | Deep Proof Search in MELL. Ozan Kahramanogullari |
| 2017 | First-Order Interpolation and Interpolating Proof Systems. Laura Kovács, Andrei Voronkov |
| 2017 | Formally Proving the Boolean Pythagorean Triples Conjecture. Luís Cruz-Filipe, Peter Schneider-Kamp |
| 2017 | From SAT to Maximum Independent Set: A New Approach to Characterize Tractable Classes. Yazid Boumarafi, Lakhdar Sais, Yakoub Salhi |
| 2017 | Gödel logics and the fully boxed fragment of LTL. Matthias Baaz, Norbert Preining |
| 2017 | Higher order interpretation for higher order complexity. Emmanuel Hainry, Romain Péchoux |
| 2017 | LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017 Thomas Eiter, David Sands |
| 2017 | On the Interaction of Inclusion Dependencies with Independence Atoms. Miika Hannula, Juha Kontinen, Sebastian Link |
| 2017 | Parallel Graph Rewriting with Overlapping Rules. Rachid Echahed, Aude Maignan |
| 2017 | Programming by Composing Filters. Jeffrey Fischer, Rupak Majumdar |
| 2017 | Propagators and Solvers for the Algebra of Modular Systems. Bart Bogaerts, Eugenia Ternovska, David G. Mitchell |
| 2017 | Proving uniformity and independence by self-composition and coupling. Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub |
| 2017 | Quantified Boolean Formulas: Call the Plumber! Josef Lindsberger, Alexander Maringele, Georg Moser |
| 2017 | Quantified Heap Invariants for Object-Oriented Programs. Temesghen Kahsai, Rody Kersten, Philipp Rümmer, Martin Schäf |
| 2017 | RACCOON: A Connection Reasoner for the Description Logic ALC. Dimas Melo Filho, Fred Freitas, Jens Otten |
| 2017 | Reasoning about Translation Lookaside Buffers. Hira Taqdees Syeda, Gerwin Klein |
| 2017 | Seminator: A Tool for Semi-Determinization of Omega-Automata. Frantisek Blahoudek, Alexandre Duret-Lutz, Mikulás Klokocka, Mojmír Kretínský, Jan Strejcek |
| 2017 | Synchronizing Constrained Horn Clauses. Dmitry Mordvinov, Grigory Fedyukovich |
| 2017 | TacticToe: Learning to Reason with HOL4 Tactics. Thibault Gauthier, Cezary Kaliszyk, Josef Urban |
| 2017 | Theorem Provers For Every Normal Modal Logic. Tobias Gleißner, Alexander Steen, Christoph Benzmüller |
| 2017 | Towards a Semantics of Unsatisfiability Proofs with Inprocessing. Tobias Philipp, Adrián Rebola-Pardo |