ITP PROGRAM
Days: Sunday, August 7th Monday, August 8th Tuesday, August 9th Wednesday, August 10th
Sunday, August 7th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:30-09:00Coffee & Refreshments
09:00-10:00 Session 85D: Invited Talk
Chair:
| 09:00 | (Invited) Modelling and Verifying Properties of Biological Neural Networks (abstract) |
10:30-11:00Coffee Break
11:00-12:00 Session 89: Keynote
Chair:
Location: Churchill Auditorium
| 11:00 | Harnessing the Power of Formal Verification for the $Trillion Chip Design Industry (abstract) |
12:30-14:00Lunch Break
Lunches will be held in Taub lobby (CAV, CSF) and in The Grand Water Research Institute (DL, NMR, ITP).
14:00-15:30 Session 90D
Chair:
| 14:00 | Candle: A Verified Implementation of HOL Light (abstract) PRESENTER: Oskar Abrahamsson |
| 14:30 | A Verified Cyclicity Checker (abstract)  PRESENTER: Arve Gengelbach |
| 15:00 | Kalas: A Verified, End-to-End Compiler for a Choreographic Language (abstract) PRESENTER: Alejandro Gómez-Londoño |
15:30-16:00Coffee Break
16:00-17:30 Session 92D
Chair:
| 16:00 | Formalized functional analysis with semilinear maps (abstract) PRESENTER: Frédéric Dupuis |
| 16:30 | Formalising Fisher’s Inequality: Formal Linear Algebraic Techniques in Combinatorics (abstract) PRESENTER: Chelsea Edmonds |
| 17:00 | Formalization of a Stochastic Approximation Theorem (abstract) PRESENTER: Koundinya Vajjha |
17:30-18:45 Session 93: Logic Lounge: Future of Autonomous Driving; Keynote by Shai Shalev-Shwartz (Mobileye and The Hebrew University of Jerusalem); Panel: Gila Kamhi (Intel, Haifa), Sanjit Seshia (UC Berkeley)
Chair:
Location: Churchill Auditorium
Monday, August 8th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:30-09:00Coffee & Refreshments
09:00-10:30 Session 94E
Chair:
| 09:00 | Refinement of Parallel Algorithms down to LLVM (abstract) |
| 09:30 | Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification (abstract)  PRESENTER: Hrutvik Kanabar |
| 10:00 | Dandelion: Certified Approximations of Elementary Functions (abstract) PRESENTER: Heiko Becker |
10:30-11:00Coffee Break
11:00-12:30 Session 96E
Chair:
| 11:00 | Synthetic Kolmogorov Complexity in Coq (abstract) PRESENTER: Yannick Forster |
| 11:30 | Formalizing Szemerédi's Regularity Lemma in Lean (abstract) PRESENTER: Yaël Dillies |
| 12:00 | Formalizing the divergence theorem and the Cauchy integral formula in Lean (abstract) |
12:30-14:00Lunch Break
Lunches will be held in Taub lobby (CAV, CSF) and in The Grand Water Research Institute (DL, NMR, IJCAR, ITP).
14:00-15:30 Session 97E
Chair:
| 14:00 | Deeper Shallow Embeddings (abstract) PRESENTER: Jacob Prinz |
| 14:30 | Compositional Verification of Interacting Systems using Event Monads (abstract) PRESENTER: Bohua Zhan |
| 15:00 | Reflexive tactics for algebra, revisited (abstract) |
15:30-16:00Coffee Break
18:30-20:30 Walking tour (at Haifa)
pickup at 18:00 from the Technion (Tour at Haifa, no food will be provided)
Tuesday, August 9th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:30-09:00Coffee & Refreshments
09:00-10:30 Session 100E
Chair:
| 09:00 | Formalization of Randomized Approximation Algorithms for Frequency Moments (abstract) |
| 09:30 | Mechanizing Soundness of Off-Policy Evaluation (abstract) PRESENTER: Jared Yeager |
| 10:00 | Formalizing Algorithmic Bounds in the Query Model in EasyCrypt (abstract) PRESENTER: Alley Stoughton |
10:30-11:00Coffee Break
11:00-12:30 Session 102E
Chair:
| 11:00 | Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL (abstract) PRESENTER: Asta Halkjær From |
| 11:30 | Undecidability of Dyadic First-Order Logic in Coq (abstract) PRESENTER: Johannes Hostert |
| 12:00 | Computational Back-and-Forth Arguments in Constructive Type Theory (abstract) |
12:30-14:00Lunch Break
Lunches will be held in Taub lobby (CAV, CSF) and in The Grand Water Research Institute (DL, NMR, IJCAR, ITP).
14:00-15:30 Session 104E
Chair:
| 14:00 | A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(r) (abstract) PRESENTER: Jagadish Bapanapally |
| 14:30 | Formalizing the ring of adèles of a global field (abstract) |
| 15:00 | Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) using the Coq Proof Assistant (abstract) |
16:00-16:30Coffee Break
16:30-17:30 Session 108: Plenary
Chair:
Location: Churchill Auditorium
| 16:30 | SMT-based Verification of Distributed Network Control Planes (abstract) |
Wednesday, August 10th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:30-09:00Coffee & Refreshments
09:00-10:30 Session 110E
Chair:
| 09:00 | (Invited) User Interface Design in the HolPy Theorem Prover (abstract) |
| 10:00 | Accelerating Verified-Compiler Development with a Verified Rewriting Engine (abstract) PRESENTER: Jason Gross |
10:30-11:00Coffee Break
11:00-12:30 Session 112E
Chair:
| 11:00 | Seventeen Provers under the Hammer (abstract) PRESENTER: Martin Desharnais |
| 11:30 | The Isabelle ENIGMA (abstract) PRESENTER: Zarathustra Goertzel |
| 12:00 | Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq (abstract) PRESENTER: Jason Gross |
12:30-14:00Lunch Break
Lunches will be held in Taub lobby (CAV, CSF) and in The Grand Water Research Institute (DL, IJCAR, ITP).
14:00-15:30 Session 115D
Chair:
| 14:00 | Use and abuse of instance parameters in the Lean mathematical library (abstract) |
| 14:30 | The Zoo of Lambda-Calculus Reduction Strategies, and Coq (abstract) PRESENTER: Tomasz Drab |
| 15:00 | Formalizing the set of primes as an alternative to the DPRM theorem (short paper) (abstract) PRESENTER: Cezary Kaliszyk |
15:30-16:00Coffee Break