| 2023 | Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs. | Jan-Christoph Kassing, Jrgen Giesl |
| 2023 | A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus. | Andrzej Indrzejczak, Yaroslav I. Petrukhin |
| 2023 | Program Synthesis in Saturation. | Petra Hozzov, Laura Kovcs, Chase Norman, Andrei Voronkov |
| 2023 | Proving Termination of C Programs with Lists. | Jera Hensel, Jrgen Giesl |
| 2023 | Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT. | Elisabeth Henkel, Jochen Hoenicke, Tanja Schindler |
| 2023 | COOL 2 - A Generic Reasoner for Modal Fixpoint Logics (System Description). | Oliver Grlitz, Daniel Hausmann, Merlin Humml, Dirk Pattinson, Simon Prucker, Lutz Schrder |
| 2023 | Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper). | Florian Frohn, Jrgen Giesl |
| 2023 | A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper). | Mathias Fleury, Peter Lammich |
| 2023 | Reasoning About Regular Properties: A Comparative Study. | Toms Fiedor, Luks Holk, Martin Hruska, Adam Rogalewicz, Juraj Sc, Pavol Vargovck |
| 2023 | SAT-Based Subsumption Resolution. | Robin Coutelier, Laura Kovcs, Michael Rawson, Jakob Rath |
| 2023 | A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification). | Yu-Fang Chen, Philipp Rmmer, Wei-Lun Tsai |
| 2023 | Formal Reasoning About Influence in Natural Sciences Experiments. | Florian Bruse, Martin Lange, Sren Mller |
| 2023 | SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning. | Martin Bromberger, Chaahat Jain, Christoph Weidenbach |
| 2023 | An Isabelle/HOL Formalization of the SCL(FOL) Calculus. | Martin Bromberger, Martin Desharnais, Christoph Weidenbach |
| 2023 | Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs. | Marvin Brieger, Stefan Mitsch, Andr Platzer |
| 2023 | QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment. | Maria Paola Bonacina, Stphane Graham-Lengrand, Christophe Vauthier |
| 2023 | Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates. | Bernard Boigelot, Pascal Fontaine, Baptiste Vergain |
| 2023 | Verified Given Clause Procedures. | Jasmin Blanchette, Qi Qiu, Sophie Tourret |
| 2023 | On Incremental Pre-processing for SMT. | Nikolaj S. Bjrner, Katalin Fazekas |
| 2023 | Superposition with Delayed Unification. | Ahmed Bhayat, Johannes Schoisswohl, Michael Rawson |
| 2023 | Certified Core-Guided MaxSAT Solving. | Jeremias Berg, Bart Bogaerts, Jakob Nordstrm, Andy Oertel, Dieter Vandesande |
| 2022 | Hypergraph-Based Inference Rules for Computing | Hui Yang, Yue Ma, Nicole Bidoit |
| 2022 | Term Orderings for Non-reachability of (Conditional) Rewriting. | Akihisa Yamada |
| 2022 | GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description). | Tanel Tammet, Dirk Draheim, Priit Jrv |
| 2022 | Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description). | Martin Suda |