Accepted Papers
| Verified Given Clause Procedures | Jasmin Blanchette, Qi Qiu and Sophie Tourret |
| Towards Fast Nominal Anti-Unification of Letrec-Expressions | Manfred Schmidt-Schauss and Daniele Nantes-Sobrinho |
| Confluence Criteria for Logically Constrained Rewrite Systems | Jonas Schöpf and Aart Middeldorp |
| A Theory of Cartesian Arrays with Applications in Quantum Circuit Verification | Yu-Fang Chen, Philipp Rümmer and Wei-Lun Tsai |
| Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs | Marvin Brieger, Stefan Mitsch and André Platzer |
| Combining Combination Properties: An Analysis of Stable-infiniteness, Convexity, and Politeness | Guilherme Toledo, Yoni Zohar and Clark Barrett |
| Superposition with Delayed Unification | Ahmed Bhayat, Michael Rawson and Johannes Schoisswohl |
| A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus | Andrzej Indrzejczak and Yaroslav Petrukhin |
| SAT-Based Subsumption Resolution | Robin Coutelier, Laura Kovacs, Michael Rawson and Jakob Rath |
| An Isabelle/HOL Formalization of the SCL(FOL) Calculus | Martin Bromberger, Martin Desharnais and Christoph Weidenbach |
| Proving Termination of C Programs with Lists | Jera Hensel and Jürgen Giesl |
| QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment | Maria Paola Bonacina, Stéphane Graham-Lengrand and Christophe Vauthier |
| Theorem Proving in Dependently-Typed Higher-Order Logic | Colin Rothgang, Florian Rabe and Christoph Benzmüller |
| Program Synthesis in Saturation | Petra Hozzová, Laura Kovács, Chase Norman and Andrei Voronkov |
| A more Pragmatic CDCL for IsaSAT and targetting LLVM | Mathias Fleury and Peter Lammich |
| Certified Core-Guided MaxSAT Solving | Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel and Dieter Vandesande |
| SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning | Martin Bromberger, Chaahat Jain and Christoph Weidenbach |
| Iscalc: an Interactive Symbolic Computation Framework (System Description) | Bohua Zhan, Yuheng Fan, Weiqiang Xiong and Runqing Xu |
| Left-Linear Completion with AC Axioms | Johannes Niederhauser, Nao Hirokawa and Aart Middeldorp |
| Choose your Colour: Tree Interpolation for Quantified Formulas in SMT | Elisabeth Henkel, Tanja Schindler and Jochen Hoenicke |
| Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic | Cláudia Nalon, Ullrich Hustadt, Fabio Papacchini and Clare Dixon |
| On Incremental Pre-processing for SMT | Nikolaj Bjorner and Katalin Fazekas |
| Proving Non-Termination by Acceleration Driven Clause Learning with LoAT – System Description | Florian Frohn and Jürgen Giesl |
| On P-interpolation in local theory extensions and applications to the study of interpolation in the description logics EL, EL+ | Dennis Peuter, Viorica Sofronie-Stokkermans and Sebastian Thunert |
| Incremental Rewriting Modulo SMT | Gerald Whitters, Boon Loo, Vivek Nigam and Carolyn Talcott |
| Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs | Jan-Christoph Kassing and Jürgen Giesl |
| Formal Reasoning about Influence in Natural Sciences Experiments | Florian Bruse, Martin Lange and Sören Möller |
| Decidability of difference logic over the reals with uninterpreted unary predicates | Baptiste Vergain, Bernard Boigelot and Pascal Fontaine |
| Reasoning about Regular Properties: A Comparative Study | Lukáš Holík, Tomas Fiedor, Adam Rogalewicz, Pavol Vargovčík, Martin Hruska and Juraj Síč |
| An Experimental Pipeline for Automated Reasoning in Natural Language | Tanel Tammet, Priit Järv, Martin Verrev and Dirk Draheim |
| COOL 2 – A Generic Reasoner for Modal Fixpoint Logics | Oliver Görlitz, Daniel Hausmann, Merlin Humml, Dirk Pattinson and Lutz Schröder |
| Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory | Lukas Stevens |
|
Verification of NP-hardness Reduction Functions for Exact Lattice Problems |
Katharina Kreuzer and Tobias Nipkow |