LPAR 2024: 25TH CONFERENCE ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE AND REASONING
PROGRAM

Days: Sunday, May 26th Monday, May 27th Tuesday, May 28th Wednesday, May 29th Thursday, May 30th Friday, May 31st

Sunday, May 26th

View this program: with abstractssession overviewtalk overview

10:30-12:30 Session 1: IWIL
Location: Master Class
10:30
Tanel Tammet (Tallinn University of Technology, Estonia)
Invited talk: Hash Indexes for Resolution-based FOL Provers (abstract)
11:20
Daniel Ranalter (University of Innsbruck, Austria)
Cezary Kaliszyk (University of Innsbruck, Austria)
User-aided Conjecturing for Automated Theorem Proving (abstract)
PRESENTER: Cezary Kaliszyk
12:00-14:00 Registration
12:30-14:00 Lunch
Location: Mosaik
14:00-16:00 Session 2: IWIL
Location: Master Class
14:00
Schulz Stephan (DHBW Stuttgart, Germany)
Shared Terms and Cached Rewriting (abstract)
14:40
Jack McKeown (University of Miami, United States)
Geoff Sutcliffe (University of Miami, United States)
Dataset-Specific Strategies for the E Theorem Prover (abstract)
PRESENTER: Jack McKeown
15:20
David Fuenmayor (University of Bamburg, Germany)
Jack McKeown (University of Miami, United States)
Geoff Sutcliffe (University of Miami, United States)
Towards StarExec in the Cloud (abstract)
PRESENTER: Geoff Sutcliffe
16:00-16:30 Break
16:00-18:00 Registration
16:30-18:00 Session 3: IWIL Panel: Software Architectures for Modern Automated Reasoning Systems - Lessons Learned?
Location: Master Class
18:00-21:00 Welcome Reception
Location: T'avola Garden
Monday, May 27th

View this program: with abstractssession overviewtalk overview

08:00-10:00 Registration
09:00-10:00 Session 4

Invited talk

Chair:
Marijn Heule (Carnegie Mellon University, United States)
Location: Master Class
09:00
Armin Biere (University of Freiburg, Germany)
30 Years of Faster and Faster SAT Solving (abstract)
10:00-10:30 Break
10:30-12:30 Session 5

SAT and applications

Chair:
Natasha Sharygina (University of Lugano, Switzerland, Switzerland)
Location: Master Class
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)
PRESENTER: Simon Schwarz
12:30-14:00 Lunch (provided)
Location: Mosaik
14:00-16:00 Session 6

Theorem Proving Unleashed

Chair:
Stephan Schulz (DHBW Stuttgart, Germany)
Location: Master Class
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 7

Verification

Chair:
Katalin Fazekas (TU Wien, Austria)
Location: Master Class
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 abstractssession overviewtalk overview

09:00-10:00 Session 8

Invited talk

Chair:
Nikolaj Bjørner (Microsoft, United States)
Location: Master Class
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 9

Theories and Logics

Chair:
Delia Kesner (Université Paris Cité, France)
Location: Master Class
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 Triolet)
14:30-16:00 Session 10

Proof Theory

Chair:
Matthias Baaz (Technische Universit"at Wien, Austria)
Location: Master Class
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 (Roma Tre and Paris Cité, IRIF, 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 University of Bozen-Bolzano, Italy)
Deep Inference in Proof Search: The Need for Shallow Inference (abstract)
16:00-16:30 Break
16:30-18:00 Session 11: Local Participants Active Research
Chair:
Geoff Sutcliffe (University of Miami, United States)
Location: Master Class
16:30
Prakash Seewoosunkur (Financial Services Commission Mauritius, Mauritius)
The Application of Artificial Intelligence in the Financial Services Sector - Risks and Opportunities (abstract)
16:40
Suraj Juddoo (Mauritius Digital Promotion Agency, Mauritius)
Mauritius as a Burgeoning AI Hub and Way Forward (abstract)
16:50
Maleika Heenaye-Mamode Khan (University of Mauritius, Mauritius)
The Potential and Future of AI in the Medical Field (abstract)
17:20
Quentin Adam (Mantu, Mauritius)
From Sugar Cane Fields to Cybercities: Data Science Bridging the Gap in Healthcare Access (abstract)
17:40
David Koon (Chinese Business Chamber, Mauritius)
Internship Opportunities in Mauritius, and Real-world Examples of AI Implementation in Business (abstract)
18:00-21:00 Local Cocktails Night
Location: Skydeck
Wednesday, May 29th

View this program: with abstractssession overviewtalk overview

08:00-18:00 Excursion
Thursday, May 30th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 12

Invited Talk

Chair:
Nikolaj Bjørner (Microsoft, United States)
Location: Master Class
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 13: Local Participants Active Research
Chair:
Geoff Sutcliffe (University of Miami, United States)
Location: Master Class
10:30
Marc Israel (Curtin Mauritius, Mauritius)
The State of AI in Mauritius: Academic and Private Sector Perspectives (abstract)
10:50
Veerajay Gooljar (Curtin Mauritius, Mauritius)
Consumer Predictive Model using Sentiment Analysis (abstract)
11:10
Lancelot de Briey (Warburg AI, Mauritius)
Creating Real-life Homologous Environments for Deep Reinforcement Learning (abstract)
11:30
Thierry Lincoln (DodoBird.AI, Mauritius)
Transfer Learning Hacks for Small Data Context: Enhancing Recommendation Systems with Limited Resources (abstract)
12:30-14:00 Lunch (provided)
Location: Mosaik
14:00-16:00 Session 14

Games and Non-classical logics

Chair:
Margus Veanes (Microsoft, United States)
Location: Master Class
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, Université Paris-Saclay, France)
François Bobot (Université Paris-Saclay, France)
Guillaume Bury (OCamlPro, France)
On SMT Theory Design: The Case of Sequences (abstract)
PRESENTER: Hichem Rami Ait El Hara
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 15

AI and Proofs

Chair:
Cezary Kaliszyk (University of Innsbruck, Austria)
Location: Master Class
16:30
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)
16:40
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:10
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:30
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 abstractssession overviewtalk overview

09:00-10:00 Session 16

Invited Talk

Chair:
Armin Biere (University of Freiburg, Germany)
Location: Master Class
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 17

Proofs and Synthesis

Chair:
Elaine Pimentel (UCL, UK)
Location: Master Class
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)
PRESENTER: Matthias Baaz
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 / bus to Mahogany Shopping Promenade)
14:30-16:00 Session 18

Tool and Short Presentation Papers

Chair:
Martin Bromberger (Max-Planck-Institut fuer Informatik, Germany)
Location: Master Class
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)
PRESENTER: Alexei Lisitsa
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 19

Short Presentation Papers

Chair:
Sophie Rain (TU Wien, Austria)
Location: Master Class
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)
PRESENTER: Joseph Zalewski
18:30-23:00 Farewell Dinner at the Beach House, Grand Baie