Program Synthesis in Saturation

Petra Hozzová, Laura Kovács, Chase Norman and Andrei Voronkov

Towards Fast Nominal anti-Unification of Letrec-Expressions

Daniele Nantes-Sobrinho and Manfred Schmidt-Schauss

Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates

Bernard Boigelot, Pascal Fontaine and Baptiste Vergain

An Experimental Pipeline for Automated Reasoning in Natural Language

Tanel Tammet, Dirk Draheim, Priit Järv and Martin Verrev

Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT

Elisabeth Henkel, Jochen Hoenicke and Tanja Schindler

Formal Reasoning About Influence in Natural Sciences Experiments

Florian Bruse, Martin Lange and Sören Möller

Confluence Criteria for Logically Constrained Rewrite Systems

Jonas Schöpf and Aart Middeldorp

Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs

Marvin Brieger, Stefan Mitsch and André Platzer

Verified Given Clause Procedures

Jasmin Blanchette, Qi Qiu and Sophie Tourret

SAT-Based Subsumption Resolution

Robin Coutelier, Laura Kovacs, Michael Rawson and Jakob Rath

Verification of NP-Hardness for Exact Lattice Problems

Katharina Kreuzer and Tobias Nipkow

Theorem Proving in Dependently-Typed Higher-Order Logic

Colin Rothgang, Florian Rabe and Christoph Benzmüller

Proving Non-Termination by Acceleration Driven Clause Learning

Florian Frohn and Jürgen Giesl

Nominal Techniques for Software Specification and Verification

Maribel Fernandez

Automated Reasoning with Data

Moshe Vardi

Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs

Jan-Christoph Kassing and Jürgen Giesl

COOL 2 - a Generic Reasoner for Modal Fixpoint Logics

Oliver Görlitz, Daniel Hausmann, Merlin Humml, Dirk Pattinson, Simon Prucker and Lutz Schröder

Superposition with Delayed Unification

Ahmed Bhayat, Johannes Schoisswohl and Michael Rawson

SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning

Martin Bromberger, Chaahat Jain and Christoph Weidenbach

An Isabelle/HOL Formalization of the SCL(FOL) Calculus

Martin Bromberger, Martin Desharnais and Christoph Weidenbach

QSMA: a New Algorithm for Quantified Satisfiability Modulo Theory and Assignment

Maria Paola Bonacina, Stéphane Graham-Lengrand and Christophe Vauthier

Left-Linear Completion with AC Axioms

Johannes Niederhauser, Nao Hirokawa and Aart Middeldorp

Lambda-Superposition: from Theory to Trophy

Jasmin Blanchette

On Incremental Pre-Processing for SMT

Nikolaj Bjorner and Katalin Fazekas

Proving Termination of C Programs with Lists

Jera Hensel and Jürgen Giesl

Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory

Lukas Stevens

A More Pragmatic CDCL for IsaSAT and Targetting LLVM

Mathias Fleury and Peter Lammich

Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic

Cláudia Nalon, Ullrich Hustadt, Fabio Papacchini and Clare Dixon

Certified Core-Guided MaxSAT Solving

Andy Oertel, Jeremias Berg, Bart Bogaerts, Jakob Nordström and Dieter Vandesande

Combining Combination Properties: an Analysis of Stable-Infiniteness, Convexity, and Politeness

Guilherme Toledo, Yoni Zohar and Clark Barrett