| 2017 | Formally Proving the Boolean Pythagorean Triples Conjecture. | Lus Cruz-Filipe, Peter Schneider-Kamp |
| 2017 | Bunched Hypersequent Calculi for Distributive Substructural Logics. | Agata Ciabattoni, Revantha Ramanayake |
| 2017 | Automated analysis of Stateflow models. | Hamza Bourbouh, Pierre-Loc Garoche, Christophe Garion, Arie Gurfinkel, Temesghen Kahsai, Xavier Thirioux |
| 2017 | From SAT to Maximum Independent Set: A New Approach to Characterize Tractable Classes. | Yazid Boumarafi, Lakhdar Sais, Yakoub Salhi |
| 2017 | Seminator: A Tool for Semi-Determinization of Omega-Automata. | Frantisek Blahoudek, Alexandre Duret-Lutz, Mikuls Klokocka, Mojmr Kretnsk, Jan Strejcek |
| 2017 | Abduction by Non-Experts. | Nikolaj S. Bjrner, Dejan Jovanovic, Tancrde Lepoint, Philipp Rmmer, Martin Schf |
| 2017 | A Quantitative Partial Model-Checking Function and Its Optimisation. | Stefano Bistarelli, Fabio Martinelli, Ilaria Matteucci, Francesco Santini |
| 2017 | Leo-III Version 1.1 (System description). | Christoph Benzmller, Alexander Steen, Max Wisniewski |
| 2017 | Decidable linear list constraints. | Sabine Bauer, Martin Hofmann |
| 2017 | Proving uniformity and independence by self-composition and coupling. | Gilles Barthe, Thomas Espitau, Benjamin Grgoire, Justin Hsu, Pierre-Yves Strub |
| 2017 | Gdel logics and the fully boxed fragment of LTL. | Matthias Baaz, Norbert Preining |
| 2017 | Decidability of Fair Termination of Gossip Protocols. | Krzysztof R. Apt, Dominik Wojtczak |
| 2017 | Propagators and Solvers for the Algebra of Modular Systems. | Bart Bogaerts, Eugenia Ternovska, David G. Mitchell |
| 2015 | Experiments with State-of-the-art Automated Provers on Problems in Tarskian Geometry. | Josef Urban, Robert Veroff |
| 2015 | Synchronized Recursive Timed Automata. | Yuya Uezato, Yasuhiko Minamide |
| 2015 | The Thousands of Models for Theorem Provers (TMTP) Model Library - First Steps. | Geoff Sutcliffe, Stephan Schulz |
| 2015 | There Is No Best \beta -Normalization Strategy for Higher-Order Reasoners. | Alexander Steen, Christoph Benzmller |
| 2015 | Analyzing Internet Routing Security Using Model Checking. | Adi Sosnovich, Orna Grumberg, Gabi Nakibly |
| 2015 | TIP: Tools for Inductive Provers. | Dan Rosn, Nicholas Smallbone |
| 2015 | Functional Pearl: the Proof Search Monad. | Jonathan Protzenko |
| 2015 | A Labelled Sequent Calculus for Intuitionistic Public Announcement Logic. | Shoshin Nomura, Katsuhiko Sano, Satoshi Tojo |
| 2015 | Focused Labeled Proof Systems for Modal Logic. | Dale Miller, Marco Volpe |
| 2015 | A New Proof of P-time Completeness of Linear Lambda Calculus. | Satoshi Matsuoka |
| 2015 | Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination. | Florian Lonsing, Fahiem Bacchus, Armin Biere, Uwe Egly, Martina Seidl |
| 2015 | On Reducing Clause DataBase in Glucose. | Chu Min Li, Fan Xiao, Ruchu Xu |