CADE-29: 29TH INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION
SLIDES

Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs

Marvin Brieger, Stefan Mitsch and André Platzer

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

Proving Non-Termination by Acceleration Driven Clause Learning

Florian Frohn and Jürgen Giesl

Certified Core-Guided MaxSAT Solving

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

A More Pragmatic CDCL for IsaSAT and Targetting LLVM

Mathias Fleury and Peter Lammich

Left-Linear Completion with AC Axioms

Johannes Niederhauser, Nao Hirokawa and Aart Middeldorp

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

Nominal Techniques for Software Specification and Verification

Maribel Fernandez

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

Jan-Christoph Kassing 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

Superposition with Delayed Unification

Ahmed Bhayat, Johannes Schoisswohl and Michael Rawson

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

Martin Bromberger, Martin Desharnais and Christoph Weidenbach

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
Total: 21 presentations.