| 8:30am-9:00am |
Breakfast and Registration |
|
|
| 9:00am-9:10am |
Opening Remarks |
Clark Barrett |
Director of Centaur |
|
Session I
|
| 9:10am-9:30am |
AI-Assisted Formal Verification |
Clark Barrett |
Director of Centaur |
| 9:30am-9:50am |
Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4 |
Leni Aniva |
PhD Student |
| 9:50am-10:20am |
Coffee break |
|
|
|
Session II
|
| 10:20am-10:40am |
Faithful Autoformalization via Roundtrip Verification and Repair |
Daneshvar Amrollahi |
PhD Student |
| 10:40am-11:00am |
Extending the cvc5 Relational Solver with Cyclicity Reasoning |
Rachel Cleaveland |
PhD Student |
| 11:00am-11:20am |
Satisfiability Modulo Extensional Constant Arrays |
Mathias Preiner |
Senior Research Scientist |
| 11:20am-11:50am |
Coffee break |
|
|
|
Session III
|
| 11:50am-12:20pm |
Lightning Talks |
|
|
| 12:20pm-2:20pm |
Lunch and Poster Session |
|
|
|
Session IV
|
| 2:20pm-2:40pm |
Automating Bitvector and Finite Field Equivalence Proofs in Lean |
Elizaveta Pertseva |
PhD Student |
| 2:40pm-3:00pm |
Branch-and-Bound for Scalable Verification of Nonlinear Neural Feedback Systems |
Samuel Akinwande |
PhD Student |
| 3:00pm-3:20pm |
Lean Automation: An Update |
Abdalrhman Mohamed |
PhD Student |
| 3:20pm-3:50pm |
Coffee break |
|
|
|
Session V
|
| 3:50pm-4:10pm |
Pono 2.0: A Versatile SMT-Based Model Checker for Safety and Liveness |
Áron Ricardo Perez-Lopez |
PhD Student |
| 4:10pm-4:30pm |
Isabelle Automation: An Update |
Hanna Lachnitt |
PhD Student |
| 4:30pm-4:50pm |
An AI-Assisted Procedure for Inductively Strengthening Invariants for Functional Hardware Verification. |
Daniel Mendoza |
PhD Student |
| 4:50pm-5:00pm |
Closing Remarks |
Clark Barrett |
Director of Centaur |
|
Reception
|
| 5:00pm-7:00pm |
Reception |
