IJCAR — PROGRAM

Days: Sunday, 26 July 2026 Monday, 27 July 2026 Tuesday, 28 July 2026 Wednesday, 29 July 2026

Sunday, 26 July 2026
10:00-11:00 Coffee Break IJCAR
Location: B2.04
11:00-12:00 Differential Equations & Hybrid Systems IJCAR
Location: B2.04
11:00-11:20
A Deductive Refinement Calculus for Differential-Algebraic Programs (abstract) 20 min
Jonathan Hellwig1, Long Qian2, André Platzer1
1 Karlsruhe Institute of Technology
2 Carnegie Mellon University
11:20-11:40
Refactoring-as-Propositions: Proved Refactoring of Hybrid Systems via Proved Refinements (abstract) 20 min
Enguerrand Prebet1, André Platzer1
1 Karlsruhe Institute of Technology
11:40-12:00
Complete Robust Hybrid Systems Reachability (abstract) 20 min
Noah Abou El Wafa1, André Platzer1
1 Karlsruhe Institute of Technology
12:00-14:00 Lunch IJCAR
Location: B2.04
14:00-14:40 Arrays & Interpolation IJCAR
Session Chair:
Carsten Lutz
Location: B2.04
14:00-14:20
Accelerating Loops with Arrays (abstract) 20 min
Florian Frohn1, Jürgen Giesl1
1 RWTH Aachen University
14:20-14:40
Saving Craig in the Fluted Fragment (abstract) 20 min
Hongkai Yin1
1 Central European University
14:40-16:00 Awards IJCAR
Session Chair:
Jürgen Giesl
Location: B2.04
14:40-14:50
Presentation of the Best Paper Award (abstract) 10 min
Carsten Lutz1, Sara Negri2
1 Leipzig University, Germany
2 Università degli Studi di Genova, Italy
14:50-15:00
Presentation of the Best Student Paper Award (abstract) 10 min
Carsten Lutz1, Sara Negri2
1 Leipzig University, Germany
2 Università degli Studi di Genova, Italy
15:00-15:10
Presentation of the Bill McCune PhD Award (abstract) 10 min
Viorica Sofronie-Stokkermans1, Pascal Fontaine2, Carsten Fuhs3, Ullrich Hustadt4, Mikoláš Janota5, Cezary Kaliszyk6, Philipp Rümmer7, Sophie Tourret8
1 University of Koblenz
2 University of Lorraine
3 Birkbeck, University of London
4 University of Liverpool
5 Czech Technical University in Prague
6 University of Melbourne
7 University of Regensburg
8 Max Planck Institute for Informatics
15:10-15:50
Herbrand Award Acceptance Speech (abstract) 40 min
Frank Pfenning1
1 Carnegie Mellon University
15:50-16:00
Presentation of the Herbrand Award (abstract) 10 min
Nikolaj Bjørner1, Amy Felty2, Cynthia Kop3, Cláudia Nalon4, Andrew Reynolds5, Geoff Sutcliffe6
1 Microsoft Research
2 University of Ottawa
3 Radboud University Nijmegen
4 University of Brasília
5 University of Colorado Boulder
6 University of Miami
16:00-16:30 Coffee Break IJCAR
Location: B2.04
Monday, 27 July 2026
09:00-10:00 Invited Talk IJCAR
Location: B2.04
09:00-10:00
A Type-Theoretic Framework for Meta-Programming: Lessons Learned from Writing Meta-Theoretic Proofs as Programs (abstract) 60 min
Brigitte Pientka1
1 McGill University, Montreal, Canada
10:00-11:00 Coffee Break IJCAR
Location: B2.04
10:00-11:00 ProoVer Competition Kickoff IJCAR
10:00-11:00
The ProoVer 2026 Competition (abstract) 60 min
Julie Cailler1, Simon Guilloud2
1 University of Lorraine & Inria
2 EPFL
10:00-11:00 CASC Competition Kickoff IJCAR
10:00-11:00
The ProoVer 2026 Competition (abstract) 60 min
Julie Cailler1, Simon Guilloud2
1 University of Lorraine & Inria
2 EPFL
11:00-12:00
The CADE ATP System Competition (abstract) 60 min
Geoff Sutcliffe1
1 University of Miami
11:00-12:00 Automation & Unification IJCAR
Location: B2.04
11:00-11:20
Unification of Deterministic Higher-Order Patterns (abstract) 20 min
Johannes Niederhauser1, Aart Middeldorp1
1 University of Innsbruck
11:20-11:40
Automating proof search when equality is a logical connective (abstract) 20 min
Kaustuv Chaudhuri1,2, Arunava Gantait1,2, Dale Miller1,2
1 Inria-Saclay & LIX
2 IPP
11:40-11:50
SMT-Based Deontic Reasoning for Aqvist Logics (abstract) 10 min
Christian Köll1, Agata Ciabattoni1, Dmitry Rozplokhas1
1 TU Wien
11:50-12:00
grind: An SMT-Inspired Tactic for Lean 4 (abstract) 10 min
Kim Morrison1, Leonardo de Moura2
1 Lean FRO
2 Amazon Web Services, and Lean FRO
12:00-14:00 Lunch IJCAR
Location: B2.04
14:00-16:00 Formalization & Interactive Proof IJCAR
Location: B2.04
14:00-14:20
A Unified Formalization of Context-Free Grammar Theory (abstract) 20 min
Tobias Nipkow1, Fabian Lehr1, Moritz Roos1, Akihisa Yamada2
1 Technical University of Munich
2 AIST
14:20-14:40
Towards Term-based Verification of Diagrammatic Equivalence (abstract) 20 min
Julie Cailler1, Noé Delorme2, Simon Perdrix2, Sophie Tourret2
1 University of Lorraine, CNRS, INRIA, LORIA
2 INRIA
14:40-15:00
Pitts and Intuitionistic Multi-Succedent: Uniform Interpolation for KM (abstract) 20 min
Hugo Férée1, Ian Shillito2
1 Université Paris Cité
2 University of Birmingham
15:00-15:20
Formally Verified Graph Generation with SAT modulo Symmetries and Lean (abstract) 20 min
Markus Kirchweger1, Pablo Manrique1, Stefan Szeider1
1 TU Wien
15:20-15:40
Semantics for Dependently-Typed Higher-Order Logic (abstract) 20 min
Florian Rabe1
1 FAU Erlangen-Nürnberg
15:40-16:00
Growing HOLMS: A Verified Automated Prover for Grzegorczyk Logic in HOL Light (abstract) 20 min
Antonella Bilotta1, Marco Maggesi2, Cosimo Perini Brogi3
1 Scuola Normale Superiore di Pisa
2 University of Florence
3 IMT School for Advanced Studies Lucca
16:00-16:30 Coffee Break IJCAR
Location: B2.04
16:30-18:30 Rewriting, Automata, Verification & Fuzzy Logic IJCAR
Location: B2.04
16:30-16:50
Disproving (Positive) Almost-Sure Termination of Probabilistic Term Rewriting via Random Walks (abstract) 20 min
Jan-Christoph Kassing1, Henri Nagel1, Alexander Schlecht1, Jürgen Giesl1
1 RWTH Aachen University
16:50-17:10
Complexity and Expressivity of the Uniform Fluted Fragment (abstract) 20 min
Hongkai Yin1
1 Central European University
17:10-17:30
Complexity of reasoning in Kleene algebra with sum-of-letters hypotheses (abstract) 20 min
Stepan Kuznetsov1,2
1 Steklov Mathematical Institute of RAS
2 HSE University
17:30-17:50
Learning Computation Tree Logic with Neural Networks (abstract) 20 min
Benjamin Bordais1, Daniel Neider2, Mustafa Yalciner2
1 Université Libre de Bruxelles
2 TU Dortmund University
17:50-18:10
Toward Fast Automatic Verification of Textbook Proof Steps (abstract) 20 min
Adam Dingle1
1 Charles University
18:10-18:20
Implementing Fuzzy OSF Logic Unification and Normalization (abstract) 10 min
Gian Carlo Milanese1, Gabriella Pasi1
1 University of Milano-Bicocca
18:20-18:30
Presentation of the Termination Competition (termCOMP) Results (abstract) 10 min
Florian Frohn1, Jürgen Giesl1, Georg Moser2, Étienne Payet3, Akihisa Yamada4, Dieter Hofbauer5
1 RWTH Aachen
2 University of Innsbruck
3 Université de La Réunion
4 National Institute of Informatics
5 ASW Saarland
18:30-20:00 Business Meeting IJCAR
Location: B2.04
Tuesday, 28 July 2026
10:00-11:00 Coffee Break IJCAR
Location: B2.04
11:00-12:00 Model Finding, Certification & Synthesis IJCAR
Location: B2.04
11:00-11:20
Finite Model Finding in First-order Modal Logics (abstract) 20 min
Happy Khairunnisa Sariyanto1, Alexander Steen1, Geoff Sutcliffe2
1 University of Greifswald
2 University of Miami
11:20-11:40
Completeness of Synthesis under Realizability Assumptions using Superposition (abstract) 20 min
Márton Hajdu1, Petra Hozzová1, Laura Kovács1, Eva Wagner1
1 TU Wien
11:40-11:50
Hardware Model Checking Certification with Certifaiger and Cerbtora (abstract) 10 min
Nils Froleyks1, Emily Yu2
1 KU Leuven
2 Leiden University
11:50-12:00
Pgeon: Generating Tableau-Based Provers from Declarative Specifications of Logical Calculi (abstract) 10 min
Romain Sidhoum1, Simon Robillard1, David Delahaye1
1 LIRMM, Univ Montpellier, CNRS, Montpellier, France
12:00-14:00 Lunch IJCAR
Location: B2.04
14:00-16:00 Superposition, Saturation, Equations & Constraints IJCAR
Location: B2.04
14:00-14:20
Tao’s Equational Proof Challenge Accepted (abstract) 20 min
Lydia Kondylidou1, Jasmin Blanchette1, Marijn Heule2
1 Ludwig-Maximilians-Universität München
2 Carnegie Mellon University
14:20-14:40
Generating Theorems by Generating Proof Structures (abstract) 20 min
Christoph Wernhard1
1 University of Potsdam
14:40-15:00
Beyond Eager Encodings: A Theory-Agnostic Approach to Theory-Lemma Enumeration in SMT (abstract) 20 min
Emanuele Civini1, Gabriele Masina1, Giuseppe Spallitta2, Roberto Sebastiani1
1 University of Trento
2 Rice University
15:00-15:20
A Superposition Calculus for Separation Logic (abstract) 20 min
Tanguy Bozec1, Nicolas Peltier2
1 LMU Munich
2 CNRS LIG
15:20-15:40
Twitch: Learning Abstractions for Equational Theorem Proving (abstract) 20 min
Guy Axelrod1, Moa Johansson1, Nicholas Smallbone1
1 Chalmers University of Technology
15:40-16:00
On Constructing Most General Solutions for Parametric Constraints (abstract) 20 min
Viorica Sofronie-Stokkermans1
1 University of Koblenz
16:00-16:30 Coffee Break IJCAR
Location: B2.04
16:30-17:00 Confluence Analysis & Rewriting IJCAR
Location: B2.04
16:30-16:50
An Applicative Multiset Path Order (abstract) 20 min
Nao Hirokawa1, Teppei Saito1, Teppei Tanaka1, Wataru Yachi1
1 JAIST
16:50-17:00
The ARI Infrastructure for Automated Confluence Analysis (abstract) 10 min
Nao Hirokawa1, Aart Middeldorp2, Teppei Saito1, René Thiemann2
1 JAIST
2 University of Innsbruck
17:00-17:30 Deepak Kapur Memorial Session IJCAR
Session Chair:
Jürgen Giesl
Location: B2.04
Wednesday, 29 July 2026
09:00-10:00 Invited Talk IJCAR
Location: B2.04
09:00-10:00
Polynomial-time Deduction with Orthologic (abstract) 60 min
Viktor Kunčak1
1 EPFL, Lausanne, Switzerland
10:00-11:00 Coffee Break IJCAR
Location: B2.04
11:00-12:00 SMT Proof Production & Checking IJCAR
Location: B2.04
11:00-11:20
A General Approach for SMT Proof Skeletons (abstract) 20 min
Joseph E. Reeves1, Haniel Barbosa2, Andrew Reynolds3, Marijn J. H. Heule1
1 Carnegie Mellon University
2 Universidade Federal de Minas Gerais
3 The University of Iowa
11:20-11:40
Automatically Translating Proof Systems for SMT Solvers to the λΠ-calculus (abstract) 20 min
Ciarán Dunne1, Guillaume Burel2
1 Télécom SudParis
2 ensIIE
11:40-11:50
Checking Regular Expressions in cvc5 Proofs (abstract) 10 min
Ofec Israel1, Yoni Zohar1, Hitarth Singh2, Bruno Dutertre3, Andrew Reynolds4, Clark Barrett5, Cesare Tinelli4
1 Bar-Ilan University
2 The Hong Kong University Of Science And Technology
3 Amazon Web Services
4 University of Iowa
5 Stanford University
11:50-12:00
Ethos: A Fast Proof Checker for the Eunoia Logical Framework (abstract) 10 min
Andrew Reynolds1, Hans-Jörg Schurr1, Mallku Soldevila2, Haniel Barbosa2, Cesare Tinelli1, Clark Barrett3
1 University of Iowa
2 Universidade Federal de Minas Gerais
3 Stanford University
12:00-13:30 Lunch IJCAR
Location: B2.04
13:30-15:30 Theory Combination, Arithmetic Circuits & Embedded Systems IJCAR
Location: B2.04
13:30-13:50
The termination of Nielsen transformations applied to word equations with length constraints (abstract) 20 min
Benjamin Przybocki1, Clark Barrett2
1 Carnegie Mellon University
2 Stanford University
13:50-14:10
Bringing closure to theory combination properties (abstract) 20 min
Guilherme Vicentin de Toledo1, Benjamin Przybocki2, Yoni Zohar3
1 Bar Ilan University
2 Carnegie Mellon University
3 Bar-Ilan University
14:10-14:30
Free Set Theory -- Cut Elimination and Consistency (abstract) 20 min
Andrzej Indrzejczak1
1 University of Lodz
14:30-14:50
Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits (abstract) 20 min
Clemens Hofstadler1, Daniela Kaufmann2, Chen Chen3
1 JKU Linz
2 TU Wien
3 Hong Kong University of Science and Technology (Guangzhou)
14:50-15:10
A Two-Watched Literal Scheme for First-Order Logic (abstract) 20 min
Yasmine Briefs1, Martin Bromberger1, Tobias Gehl1, Lorenz Leutgeb1, Simon Schwarz1, Christoph Weidenbach1
1 Max Planck Institute for Informatics
15:10-15:30
Verification of Configurable SRA Systems (abstract) 20 min
Alessandro Cimatti1, Alberto Griggio1, Christian Lidström1, Gianluca Redondi1, Dylan Trenti1
1 Fondazione Bruno Kessler
15:30-16:00 Coffee Break IJCAR
Location: B2.04
16:00-18:00 Refined Logics & Proofs, Hyperproperties & Synthesis IJCAR
Location: B2.04
16:00-16:20
Proof Nets for PiL (abstract) 20 min
Matteo Acclavio1, Giulia Manara1
1 University of Southern Denmark
16:20-16:40
Ordered Adjoint Logic (abstract) 20 min
Sophia Roshal1, Frank Pfenning1
1 Carnegie Mellon University
16:40-17:00
A Complete Proof System for HyperLTL (abstract) 20 min
Naijun Zhan1, Wen Tang2, Dimitar Guelev3
1 School of Computer Science, Peking University
2 Department of Philosophy, Peking University, Beijing, China
3 Institute of Mathematics and Informatics, Bulgarian Academy of Sciences, Sofia, Bulgaria
17:00-17:20
Automatic Abstraction Refinement for Hyperproperties Verification (abstract) 20 min
Malak Marrid1, Shachar Itzhaky1, Sharon Shoham2, Yakir Vizel1
1 The Technion
2 Tel Aviv University
17:20-17:40
Uniform interpolation with constructive diamond (abstract) 20 min
Iris van der Giessen1, Ian Shillito2
1 University of Amsterdam
2 University of Birmingham
17:40-18:00
Program Synthesis for Non-Linear Real Arithmetic: Beyond Realizable Specifications (abstract) 20 min
S. Akshay1, Supratik Chakraborty1, Aniruddha Joshi2, R. Govind3
1 IIT Bombay
2 University of California Berkeley
3 The Institute of Mathematical Sciences
Designed and Developed by EventKey | Copyright 2026 EventKey Last updated:
🔍 ↑