Martin Giese | Industrial Data Access | | |

Erika Abraham | Symbolic Computation Techniques in SMT Solving: Mathematical Beauty meets Efficient Heuristics | | |

Jean Marie Lagniez, Daniel Le Berre, Tiago de Lima and Valentin Montmirail | An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem | | Jul 14 14:00 |

Yizheng Zhao and Renate A. Schmidt | FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics | | Jul 14 16:30 |

Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes and Uwe Waldmann | Superposition for Lambda-Free Higher-Order Logic | | Jul 16 11:30 |

Miika Hannula and Sebastian Link | Automated Reasoning about Key Sets | | Jul 17 11:30 |

Michael Peter Lettmann and Nicolas Peltier | A Tableaux Calculus for Reducing Proof Size | | Jul 15 10:00 |

Franziska Rapp and Aart Middeldorp | FORT 2.0 | | Jul 17 15:15 |

Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel and Uwe Waldmann | Formalizing Bachmair and Ganzinger's Ordered Resolution Prover | | Jul 15 12:00 |

Alexander Steen and Christoph Benzmüller | The Higher-Order Prover Leo-III | | Jul 17 14:00 |

Jeremy Dawson, Nachum Dershowitz and Rajeev Gore | Well-Founded Unions | | Jul 15 15:00 |

Katalin Fazekas, Fahiem Bacchus and Armin Biere | Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories | | Jul 14 11:30 |

Sylvain Conchon, David Declerck and Fatiha Zaidi | Cubicle-W: Parameterized Model Checking on Weak Memory | | Jul 17 14:30 |

Florian Lonsing and Uwe Egly | QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property | | Jul 15 09:00 |

Guillaume Melquiond and Raphaël Rieu-Helft | A Why3 framework for reflection proofs and its application to GMP's algorithms | | Jul 15 17:30 |

Marcelo Finger and Sandro Preto | Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic | | Jul 17 11:00 |

André Platzer | Uniform Substitution for Differential Game Logic | | Jul 15 17:00 |

Max Kanovich, Stepan Kuznetsov, Vivek Nigam and Andre Scedrov | A Logical Framework with Commutative and Non-Commutative Subexponentials | | Jul 15 16:30 |

Peter Backeman, Aleksandar Zeljić, Christoph M. Wintersteiger and Philipp Rümmer | Exploring Approximations for Floating-Point Arithmetic using UppSAT | | Jul 15 11:00 |

Manuel Bodirsky and Johannes Greiner | Complexity of Combinations of Qualitative Constraint Satisfaction Problems | | Jul 16 09:30 |

Mnacho Echenim, Nicolas Peltier and Yanis Sellami | A Generic Framework for Implicate Generation Modulo Theories | | Jul 14 12:00 |

Stefan Ciobaca and Dorel Lucanu | A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems | | Jul 14 16:00 |

Cunjing Ge, Feifei Ma, Tian Liu, Jian Zhang and Xutong Ma | A New Probabilistic Algorithm for Approximate Model Counting | | Jul 14 15:00 |

Martin Bromberger | A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems | | Jul 15 12:00 |

Nao Hirokawa, Julian Nagele and Aart Middeldorp | Cops and CoCoWeb: Infrastructure for Confluence Tools | | Jul 17 15:00 |

Pei Huang, Feifei Ma, Jian Zhang, Cunjing Ge and Hantao Zhang | Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing | | Jul 14 14:30 |

Jasmin Christian Blanchette, Nicolas Peltier and Simon Robillard | Superposition with Datatypes and Codatatypes | | Jul 16 11:00 |

Nicholas Smallbone and Koen Claessen | Efficient encodings of first-order Horn formulas in equational logic | | Jul 16 12:00 |

Evgenii Kotelnikov, Laura Kovacs and Andrei Voronkov | A FOOLish Encoding of the Next State Relations of Imperative Programs | | Jul 15 16:30 |

Dominique Larchey-Wendling | Constructive Decision via Redundancy-free Proof-Search | | Jul 15 11:00 |

Nicolas Jeannerod and Ralf Treinen | Deciding the First-Order Theory of an Algebra of Feature Trees with Updates | | Jul 16 09:00 |

Jens Katelaan, Dejan Jovanović and Georg Weissenbacher | A Separation Logic with Data: Small Models and Automation | | Jul 17 10:00 |

Sarah Winkler and Georg Moser | MaedMax: A Maximal Ordered Completion Tool | | Jul 17 14:45 |

Matteo Acclavio and Lutz Strassburger | From Syntactic Proofs to Combinatorial Proofs | | Jul 15 16:00 |

Cláudia Nalon and Dirk Pattinson | A Resolution-Based Calculus for Preferential Logics | | Jul 15 09:00 |

Benjamin Kiesl, Adrian Rebola-Pardo and Marijn Heule | Extended Resolution Simulates DRAT | | Jul 15 09:30 |

Bohua Zhan and Maximilian P. L. Haslbeck | Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle | | Jul 15 11:30 |

Jochen Hoenicke and Tanja Schindler | Efficient Interpolation for the Theory of Arrays | | Jul 14 11:00 |

Bartosz Piotrowski and Josef Urban | ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback | | Jul 17 14:15 |

Dennis Müller, Florian Rabe and Michael Kohlhase | Theories as Types | | Jul 15 17:30 |

Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli and Clark Barrett | Datatypes with Shared Selectors | | Jul 15 11:30 |

Yevgeny Kazakov and Peter Skočovský | Enumerating Justifications using Resolution | | Jul 15 09:30 |

Alexey Ignatiev, Filipe Pereira, Nina Narodytska and Joao Marques-Silva | A SAT-Based Approach to Learn Explainable Decision Sets | | Jul 15 10:00 |

Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan and Michael Norrish | Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions | | Jul 15 17:00 |

Julio Cesar Lopez Hernandez and Konstantin Korovin | An abstraction-refinement framework for reasoning with large theories | | Jul 17 12:00 |

Jacopo Urbani, Markus Krötzsch, Ceriel Jacobs, Irina Dragoste and David Carral | Efficient Model Construction for Horn Logic with VLog: System Description | | Jul 14 16:45 |

Anupam Das | Focussing, MALL and the polynomial hierarchy | | Jul 16 10:00 |

Etienne Payet and Fausto Spoto | Checking Array Bounds by Abstract Interpretation and Symbolic Expressions | | Jul 15 16:00 |