PROGRAM
Days: Sunday, October 25th Monday, October 26th Tuesday, October 27th Wednesday, October 28th Thursday, October 29th Friday, October 30th
Sunday, October 25th
View this program: with abstractssession overviewtalk overview
11:00-12:30 Session 1: IWIL 1
Chair:
| 11:00 | Opening (abstract) PRESENTER: Stephan Schulz |
| 11:10 | Building Blocks for Reasoning on the BEAM (abstract) PRESENTER: Johannes Schuster |
| 11:50 | An Implementation of Integer Presburger Arithmetic in a Math Education Tool (abstract) PRESENTER: Mika Hirvensalo |
14:30-16:00 Session 2: IWIL 2
Chair:
| 14:30 | Algebraic Indexing to Parallelize Atom Comparison in the ATP Saturation Loop (abstract) PRESENTER: Theodore Kim |
| 15:10 | Some Experiments with Twee-Style Goal-Directedness (abstract) |
16:30-18:00 Session 3: IWIL 3
Chair:
| 16:30 | Efficient Linear Model Building and Clause Evaluation (abstract) PRESENTER: Simon Schwarz |
| 17:05 | Benchmarking LLMs Against TPTP: A Vision for the Near Future (abstract) PRESENTER: Andrija Urošević |
Monday, October 26th
View this program: with abstractssession overviewtalk overview
10:00-11:00 Session 4: invited talk
Chair:
| 10:00 | NetKAT: Learning Models and Solving Equations (abstract) |
11:30-12:20 Session 5: Benchmarks
Chair:
| 11:30 | Challenging Benchmarks for Diagrammatic Equivalence of Circuits in TPTP and SMT-LIB (abstract) |
| 12:00 | Thousands of Problems to Lean (abstract) |
14:30-16:00 Session 6: Formalisation I
Chair:
| 14:30 | Aligning HOL-Light and Rocq libraries formally (abstract) |
| 15:00 | Formal Verification of Proofs from Automated Theorem Provers for Higher-Order Logic (abstract) |
| 15:30 | Formalized Hopfield Networks and Boltzmann Machines (abstract) |
16:30-18:00 Session 7: Formalisation II
Chair:
| 16:30 | Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean (abstract) |
| 17:00 | A Minimalist Approach to Trustworthy Programming with Precise Types using Small Inversions (abstract) |
| 17:30 | A Formalized Neurodynamic Solver for $N$-Queens Completion (abstract) |
Tuesday, October 27th
View this program: with abstractssession overviewtalk overview
09:00-10:00 Session 8: invited talk
Chair:
| 09:00 | Using Formal Verification for the Text-to-SQL Task (abstract) |
10:30-12:30 Session 9: Verification
Chair:
| 10:30 | Induction and K-Induction for Hyperproperties (abstract) |
| 11:00 | Reasoning About Hyperproperties with Automated Theorem Provers (abstract)  |
| 11:20 | Comparison Invariants for Verifying Control Invariance (abstract) PRESENTER: Promit Panja |
14:30-16:00 Session 10: Satisfiability I
Chair:
| 14:30 | Coloring Queens with Thousands of Encodings (abstract) |
| 15:00 | A SAT Attack on Tarski's High School Algebra Problem (abstract) |
| 15:30 | Extending SMT Solving with Non-Ground Clause Learning (abstract) |
16:30-18:00 Session 11: Satisfiability II
Chair:
| 16:30 | Compact Partial Symmetry Breaking for Graph Search Problems (abstract) |
| 17:00 | Stream Reasoning with Sequencing (abstract) PRESENTER: Alexander Artikis |
Wednesday, October 28th
View this program: with abstractssession overviewtalk overview
Thursday, October 29th
View this program: with abstractssession overviewtalk overview
10:30-12:30 Session 13: Applications of Language Models
Chair:
| 10:30 | Vibe-Coded and Tuned: A State-of-the-Art SMT Solver for QF-LRA (abstract) |
| 10:40 | Knowledge Representation and Proof Search for English-to-Logic Question Answering (abstract) |
| 11:00 | Formally Solving Answer-Construction Problems in Lean (abstract) |
| 11:30 | LLM-Assisted Formal Verification of Bit-vector Invertibility Conditions in Rocq (abstract) |
14:30-16:00 Session 14: Computation and Complexity
Chair:
| 14:30 | de Vrijer's Strong Normalization in Haskell (abstract) |
| 14:50 | Cycle Detection for Affine Integer Linear Loops (abstract) |
| 15:00 | Reintroducing the Second Player in EPR (abstract) |
| 15:30 | Maslov's class K with Equivalence (abstract) |
16:30-18:00 Session 15: Automated Deduction
Chair:
| 16:30 | Experiments on Automating Boolos Curious Inference (abstract) |
| 16:50 | Neural Conjecturing for Saturation Theorem Provers (short) (abstract) |
| 17:00 | Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification (abstract) |
| 17:30 | Teaching Vampire New Tricks: An Experimental Study of Neural Clause Selection (abstract) |
Friday, October 30th
View this program: with abstractssession overviewtalk overview
09:00-10:00 Session 16: invited talk
Chair:
| 09:00 | Bug-free embedded software: a realisable dream? (and how VerCors will help…) (abstract) |
10:30-12:30 Session 17: Modal and Description Logics, Analytic Tableaux
Chair:
| 10:30 | STLSat---An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas (abstract) PRESENTER: Michele Chiari |
| 11:00 | Subsumption in FL_⊥reg with TBox Is in ExpTime. (abstract) |
| 11:30 | First-Order Tableaux with Unification for Henkin Quantifiers (abstract) |
| 12:00 | Tight Complexity for Modal Extensions of Lec with K, 4, T (abstract) |
14:30-16:00 Session 18: Transition Systems and Automata
Chair:
| 14:30 | Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support (abstract) |
| 15:00 | Simple Complementation of Generalized Büchi Automata (abstract) |
| 15:30 | Blinking Synthesis (abstract) |
16:30-18:00 Session 19: Proofs
Chair:
| 16:30 | Scaling Zero Knowledge UNSAT Verification via Normalized Chaining (abstract) PRESENTER: Ashwin Karthikeyan |
| 17:00 | Towards a Proof-Theoretic Analysis of Incorrect/Incomplete Proofs (abstract) |
| 17:10 | Towards an Operational Proof-theoretic Semantics (abstract) |