| 2018 | LTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems. | Rachel Faran, Orna Kupferman |
| 2018 | Influence of Variables Encoding and Symmetry Breaking on the Performance of Optimization Modulo Theories Tools Applied to Cloud Resource Selection. | Madalina Erascu, Flavia Micota, Daniela Zaharie |
| 2018 | The Weak Completion Semantics and Equality. | Emmanuelle-Anna Dietz, Steffen Hlldobler, Sibylle Schwarz, L. Yohanes Stefanus |
| 2018 | Graph Path Orderings. | Nachum Dershowitz, Jean-Pierre Jouannaud |
| 2018 | Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm. | Guillaume Davy, Eric Feron, Pierre-Loc Garoche, Didier Henrion |
| 2018 | The involutions-as-principal types/application-as-unification Analogy. | Alberto Ciaffaglione, Furio Honsell, Marina Lenisa, Ivan Scagnetto |
| 2018 | Quasipolynomial Set-Based Symbolic Algorithms for Parity Games. | Krishnendu Chatterjee, Wolfgang Dvork, Monika Henzinger, Alexander Svozil |
| 2018 | Two-variable First-Order Logic with Counting in Forests. | Witold Charatonik, Yegor Guskov, Ian Pratt-Hartmann, Piotr Witkowski |
| 2018 | Reasoning About Prescription and Description Using Prioritized Default Rules. | Valentin Cassano, Carlos Areces, Pablo F. Castro |
| 2018 | Efficient SAT-Based Encodings of Conditional Cardinality Constraints. | Abdelhamid Boudane, Sad Jabbour, Badran Raddaoui, Lakhdar Sais |
| 2018 | A Verified Efficient Implementation of the LLL Basis Reduction Algorithm. | Ralph Bottesch, Max W. Haslbeck, Ren Thiemann |
| 2018 | Why These Automata Types? | Udi Boker |
| 2018 | Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets. | Jaroslav Bendk, Ivana Cerna |
| 2018 | Decidable Inequalities over Infinite Trees. | Sabine Bauer, Steffen Jost, Martin Hofmann |
| 2018 | Towards Efficient Metaquery Generator. | Tamar Bash, Rachel Ben-Eliyahu-Zohary |
| 2018 | Lyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gdel Logic. | Matthias Baaz, Anela Lolic |
| 2018 | Matching in the Description Logic FL0 with respect to General TBoxes. | Franz Baader, Oliver Fernandez Gil, Pavlos Marantidis |
| 2018 | Function Summarization Modulo Theories. | Sepideh Asadi, Martin Blicha, Grigory Fedyukovich, Antti E. J. Hyvrinen, Karine Even-Mendoza, Natasha Sharygina, Hana Chockler |
| 2018 | When Are Two Gossips the Same? | Krzysztof R. Apt, Davide Grossi, Wiebe van der Hoek |
| 2018 | Wayeb: a Tool for Complex Event Forecasting. | Elias Alevizos, Alexander Artikis, Georgios Paliouras |
| 2018 | Left-Handed Completeness for Kleene algebra, via Cyclic Proofs. | Anupam Das, Amina Doumane, Damien Pous |
| 2017 | An Interpolation-based Compiler and Optimizer for Relational Queries (System design Report). | David Toman, Grant E. Weddell |
| 2017 | Reasoning about Translation Lookaside Buffers. | Hira Taqdees Syeda, Gerwin Klein |
| 2017 | Capability Discovery for Automated Reasoning Systems. | Alexander Steen, Max Wisniewski, Hans-Jrg Schurr, Christoph Benzmller |
| 2017 | Going Polymorphic - TH1 Reasoning for Leo-III. | Alexander Steen, Max Wisniewski, Christoph Benzmller |