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