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
Monday, October 26th
View this program: with abstractssession overviewtalk overview
11:30-12:20 Session 2: Benchmarks
| 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 3: Formalisation I
| 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 4: Formalisation II
| 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 5: invited talk
| 09:00 | Using Formal Verification for the Text-to-SQL Task (abstract) |
10:30-12:30 Session 6: Verification
| 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 7: Satisfiability I
| 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 8: Satisfiability II
| 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 10: Applications of Language Models
| 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 11: Computation and Complexity
| 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 | Pushing the Limits of Decidability: Maslov's class K with Equivalence (abstract) |
16:30-18:00 Session 12: Automated Deduction
| 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 13: invited talk
| 09:00 | Bug-free embedded software: a realisable dream? (and how VerCors will help…) (abstract) |
10:30-12:30 Session 14: Modal and Description Logics, Analytic Tableaux
| 10:30 | STLSat---An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas (abstract) |
| 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 15: Transition Systems and Automata
| 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 16: Proofs
| 16:30 | Scaling Zero Knowledge UNSAT Verification via Normalized Chaining (abstract) |
| 17:00 | Towards a Proof-Theoretic Analysis of Incorrect/Incomplete Proofs (abstract) |
| 17:10 | Towards an Operational Proof-theoretic Semantics (abstract) |