| Authors | Title | Paper | Talk |
|---|
| 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 |