Program

10:30	Katalin Fazekas (TU Wien, Austria) Florian Pollitt (University of Freiburg, Germany) Mathias Fleury (University of Freiburg, Germany) Armin Biere (University of Freiburg, Germany) Certifying Incremental SAT Solving (abstract)
11:00	Bernardo Subercaseaux (Carnegie Mellon University, Chile) Sometimes Hoarding is Harder than Cleaning: NP-hardness of Maximum Blocked-Clause Addition (abstract)
11:30	Luís Cruz-Filipe (Dept. of Mathematics and Computer Science, University of Southern Denmark, Denmark) Peter Schneider-Kamp (University of Southern Denmark, Denmark) Minimizing Sorting Networks at the Sub-Comparator Level (abstract)
12:00	Martin Bromberger (Max Planck Institute for Informatics, Germany) Simon Schwarz (Max Planck Institute for Informatics, Germany) Christoph Weidenbach (Max Planck Institute for Informatics, Germany) Automatic Bit- and Memory-Precise Verification of eBPF Code (abstract)

12:30-14:00 Lunch (provided)

14:00-16:00 Session 7

Theorem Proving Unleashed

Location: Conference Room

14:00	Jelle Piepenbrock (Radboud University, Netherlands) Mikolas Janota (Czech Technical University in Prague, Czechia) Josef Urban (Czech Technical University in Prague, Czechia) Jan Jakubův (Czech Technical University in Prague, Czechia) First Experiments with Neural CVC5 (abstract)
14:20	Tanel Tammet (Tallinn University of Technology, Estonia) Waste Reduction: Experiments in Sharing Clauses between Runs of a Portfolio of Strategies (Experimental Paper) (abstract)
14:40	Lachlan McGinness (Australian National University, Australia) Peter Baumgartner (CSIRO, Australia) Automated Theorem Provers Help Improve Large Language Model Reasoning (abstract)
15:10	Kristina Aleksandrova (University of Innsbruck, Austria) Jan Jakubuv (University of Innsbruck, Austria) Cezary Kaliszyk (University of Innsbruck, Austria) Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery (abstract)
15:30	Marton Hajdu (TU Wien, Austria) Laura Kovács (TU Wien, Austria) Michael Rawson (TU Wien, Austria) Rewriting and Inductive Reasoning (abstract) PRESENTER: Marton Hajdu

16:00-16:30 Break

16:30-18:00 Session 8

Verification

Location: Conference Room

16:30	Pamina Georgiou (Vienna University of Technology, Austria) Marton Hajdu (Vienna University of Technology, Austria) Laura Kovács (TU Wien, Austria) Sorting without Sorts (abstract)
17:00	Joseph Tafese (University of Waterloo, Canada) Arie Gurfinkel (University of Waterloo, Canada) Efficient Simulation for Hardware Model Checking (abstract) PRESENTER: Joseph Tafese
17:20	Nachum Dershowitz (Tel Aviv University, Israel) Alternate Semantics of the Guarded Conditional (abstract)
17:30	Mudathir Mahgoub Yahia Mohamed (University of Iowa, United States) Andrew Reynolds (University of Iowa, United States) Cesare Tinelli (The University of Iowa, United States) Clark Barrett (Stanford University, United States) Verifying SQL queries using theories of tables and relations - virtual talk over Zoom (abstract) PRESENTER: Mudathir Mahgoub Yahia Mohamed

Tuesday, May 28th

View this program: with abstracts session overview talk overview

09:00-10:00 Session 9

Invited talk

Location: Conference Room

09:00

Erika Abraham (RWTH Aachen, Germany)

On the Idea of Exploration-guided Satisfiability Checking (abstract)

10:00-10:30 Break

10:30-12:30 Session 10

Theories and Logics

Location: Conference Room

10:30	Johannes Schoisswohl (TU Wien, Austria) Laura Kovács (TU Wien, Austria) Konstantin Korovin (The University of Manchester, UK) VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic (abstract)
11:00	Guilherme Toledo (Bar Ilan University, Israel) Yoni Zohar (Bar-Ilan University, Israel) Combining Combination Properties: Minimal Models (abstract)
11:30	Mark Chimes (TU Wien, Austria) Radu Iosif (Verimag, CNRS, University of Grenoble Alpes, France) Florian Zuleger (TU Wien, Austria) Tree-Verifiable Graph Grammars (abstract)
12:00	Matthias Lanzinger (TU Wien, Austria) Stefano Sferrazza (University of Oxford, UK) Przemysław Andrzej Wałęga (University of Oxford, UK) Georg Gottlob (University of Calabria, Italy) Fuzzy Datalog$^\exists$ over Arbitrary t-norms (abstract)

12:30-14:30 Lunch (on your own - shuttle to Pointe aux Piments and Trou-aux-Biches)

14:30-16:00 Session 11

Proof Theory

Location: Conference Room

14:30	Pablo Barenbaum (Universidad Nacional de Quilmes (CONICET) and ICC, Universidad de Buenos Aires, Argentina) Delia Kesner (Université Paris Cité, France) Mariana Milicich (Université Paris Cité, France) Hybrid Intersection Types for PCF (abstract)
15:00	Giulio Guerrieri (University of Sussex, UK) Giulia Manara (Institut de Mathématiques de Marseille, Aix-Marseille Université, France) Lorenzo Tortora de Falco (Università Roma Tre, Italy) Lionel Vaux Auclair (Aix Marseille Université, France) Confluence for Proof-Nets via Parallel Cut Elimination (abstract)
15:30	Ozan Kahramanogullari (Free Unversity of Bolzano-Bozen, Faculty of Computer Science, Italy) Deep Inference in Proof Search: The Need for Shallow Inference (abstract)

16:00-16:30 Break

16:30-18:00 Session 12: Local Participants Active Research

Location: Conference Room

18:00-21:00 Local Cocktails Night

Wednesday, May 29th

View this program: with abstracts session overview talk overview

08:00-18:00 Excursion

Thursday, May 30th

View this program: with abstracts session overview talk overview

09:00-10:00 Session 13

Invited Talk

Location: Conference Room

09:00

Joost-Pieter Katoen (RWTH Aachen University, Germany)

Probabilistic Programs. Verified. Push-Button. (abstract)

10:00-10:30 Break

10:30-12:30 Session 14: Local Participants Active Research

Location: Conference Room

12:30-14:00 Lunch (provided)

14:00-16:00 Session 15

Games and Non-classical logics

Location: Conference Room

14:00	Rolf Hennicker (LMU Munich, Germany) Alexander Knapp (University of Augsburg, Germany) Martin Wirsing (LMU Munich, Germany) Symbolic Realisation of Epistemic Processes (abstract)
14:30	Christian Fermüller (Vienna University of Technology, Austria) Robert Freiman (Vienna University of Technology, Austria) Timo Lang (University College London, UK) A Simple Token Game and its Logic (abstract)
15:00	Hichem Rami Ait El Hara (OCamlPro, France) François Bobot (Université Paris-Saclay, France) Guillaume Bury (OCamlPro, France) What makes a good theory of sequences? (abstract)
15:10	Aaron Hunter (British Columbia Institute of Technology, Canada) Alberto Iglesias (British Columbia Institute of Technology, Canada) A Tool for Reasoning about Trust and Belief (abstract)
15:30	Sophie Rain (TU Wien, Austria) Lea Salome Brugger (ETH Zürich, Switzerland) Anja Petković Komel (TU Wien, Austria) Laura Kovács (TU Wien, Austria) Michael Rawson (TU Wien, Austria) Scaling CheckMate for Game-Theoretic Security (abstract) PRESENTER: Sophie Rain

16:00-16:30 Break

16:30-18:00 Session 16

AI and Proofs

Location: Conference Room

16:30	Robert Freiman (Vienna University of Technology, Austria) Carlos Olarte (LIPN, Université Sorbonne Paris Nord, France) Elaine Pimentel (UCL, UK) Christian Fermüller (Vienna University of Technology, Austria) Reasoning About Group Polarization: From Semantic Games to Sequent Systems (abstract)
17:00	Naïm Moussaoui Remil (Inria Paris \| École Normale Supérieure, France) Caterina Urban (Inria Paris \| École Normale Supérieure, France) Antoine Miné (Sorbonne Université, CNRS, LIP6, France) Automatic Detection of Vulnerable Variables for CTL Properties of Programs (abstract) PRESENTER: Naïm Moussaoui Remil
17:20	Johann Rosain (ENS Lyon, France) Richard Bonichon (O(1) Labs, United States) Julie Cailler (University of Regensburg, Germany) Olivier Hermant (CRI, France) A Generic Deskolemization Strategy (abstract)

Friday, May 31st

View this program: with abstracts session overview talk overview

09:00-10:00 Session 17

Invited Talk

Location: Conference Room

09:00

Kuldeep Meel (University of Toronto, Canada)

Automated Synthesis: An Ideal Meeting Ground for Symbolic Reasoning and Machine Learning (abstract)

10:00-10:30 Break

10:30-12:30 Session 18

Proofs and Synthesis

Location: Conference Room

10:30	S. Akshay (IIT Bombay, India) Supratik Chakraborty (IIT Bombay, India) Amir Kafshdar Goharshady (Hong Kong University of Science and Technology, Hong Kong) R. Govind (Uppsala University, Sweden) Harshit Jitendra Motwani (Hong Kong University of Science and Technology, Hong Kong) Sai Teja Varanasi (IIT Bombay, India) Automated Synthesis of Decision Lists for Polynomial Specifications over Integers (abstract) PRESENTER: Amir Kafshdar Goharshady
11:00	Anela Lolic (TU Wien, Austria) Matthias Baaz (Technische Universität Wien, Austria) On Translations of Epsilon Proofs to LK (abstract)
11:30	Frédéric Blanqui (INRIA, France) Translating HOL-Light proofs to Coq (abstract)
12:00	Anela Lolic (TU Wien, Austria) Alexander Leitsch (Institute of Computer Languages (E185), TU Wien, Austria) Herbrand's Theorem in Inductive Proofs (abstract) PRESENTER: Anela Lolic

12:30-14:30 Lunch (on your own - shuttle to Grand Baie)

14:30-16:00 Session 19

Tool and Short Presentation Papers

Location: Conference Room

14:30	Daniel Ranalter (University of Innsbruck, Austria) Chad Brown (Czech Technical University in Prague, Czechia) Cezary Kaliszyk (University of Innsbruck, Austria) Experiments with Choice in Dependently-Typed Higher-Order Logic (abstract)
14:50	Andrew Fish (University of Liverpool, UK) Alexei Lisitsa (University of Liverpool, UK) Automated Reasoning with Tangles: towards Quantum Verification Applications (abstract)
15:00	Alexei Lisitsa (University of Liverpool, UK) Towards computer-assisted proofs of parametric Andrews-Curtis simplifications, II (abstract)
15:10	Anela Lolic (TU Wien, Austria) Alexander Leitsch (TU Wien, Austria) Stella Mahler (TU Wien, Austria) On Proof Schemata and Primitive Recursive Arithmetic (abstract) PRESENTER: Anela Lolic
15:20	Fred Mesnard (université de la Réunion, Reunion) Thierry Marianne (University of Reunion, Reunion) Etienne Payet (LIM, Université de La Réunion, Reunion) Automated Theorem Proving for Prolog Verification (abstract) PRESENTER: Fred Mesnard
15:30	Alexander Victor Gheorghiu (University College London, UK) A System for Evaluating the Admissibility of Rules for Intuitionistic Propositional Logic (abstract)
15:40	Margus Veanes (Microsoft, United States) On Symbolic Derivatives and Transition Regexes (abstract)
15:50	Martin Blicha (University of Lugano, Switzerland) Natasha Sharygina (University of Lugano, Switzerland, Switzerland) Konstantin Britikov (Universita della svizerra italiana, Switzerland) Golem: A Flexibile and Efficient Solver for Constrained Horn Clauses (abstract)

16:00-16:30 Break

16:30-18:00 Session 20

Short Presentation Papers

Location: Conference Room

16:30	Konstantin Britikov (Universita della svizerra italiana, Switzerland) Ilia Zlatkin (Deutsche Bank, United States) Grigory Fedyukovich (Florida State University, United States) Leonardo Alt (Ethereum Foundation, Germany) Natasha Sharygina (University of Lugano, Switzerland, Switzerland) Automated Test Case Generation for Solidity Using Constrained Horn Clauses (abstract)
16:40	Olivier Hermant (Mines Paris, PSL University, France) Wojciech Loboda (AGH University of Science and Technology, Poland) Numeric Base Conversion with Rewriting (abstract)
16:50	Tudor Jebelean (ICAM, University of Timisoara Romania and RISC, JKU Linz Austria, Austria) A Natural Style Prover in Theorema Using Sequent Calculus with Unit Propagation (abstract)
17:00	Joseph Zalewski (Kansas State University, United States) Pascal Hitzler (Kansas State University, United States) A Case for Extensional Non-Wellfounded Metamodeling (abstract)
17:10	Isabela Dramnesc (West University of Timisoara, Romania) Tudor Jebelean (Research Institute for Symbolic Computation (RISC), Austria) Sorin Stratulat (Université de Lorraine, Metz, France) Certification of Tail Recursive Bubble--Sort in Theorema and Coq (abstract)

18:00-22:00 Farewell Dinner