Centaur Annual Meeting 2025

Paul Brest Hall
555 Salvatierra Walk
Stanford, CA 94305

Tuesday September 23

8:30am-9:00am	Breakfast and Registration
9:00am-9:10am	Opening Remarks	Clark Barrett	Director of Centaur
Session I
9:10am-9:30am	CSLib and a Platform for Formally Verifying Everything	Clark Barrett	Director of Centaur
9:30am-9:50am	Scalable Hardware Side-Channel Discovery with Property Decomposition and Model Checkers	Caroline Trippel	Faculty
9:50am-10:20am	Coffee break
Session II
10:20am-10:40am	Verification and Synthesis of Spatial Implications for Bounding Volume Hierarchy Traversals	Nestan Tsiskaridze	Research Scientist
10:40am-11:00am	Lean SMT: An SMT Tactic for Discharging Proof Goals in Lean	Abdalrhman Mohamed	PhD Student
11:00am-11:20am	Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL	Hanna Lachnitt	PhD Student
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	Per-Instance Subproblem Generation for Strategy Selection in SMT	Amalee Wilson	PhD Student
2:40pm-3:00pm	Verifying Nonlinear Neural Feedback Systems Using Polyhedral Enclosures	Samuel Akinwande	PhD Student
3:00pm-3:20pm	Incorporating Native String Reasoning in Symbolic Execution of C Programs	Rachel Cleaveland	PhD Student
3:20pm-3:50pm	Coffee break
Session V
3:50pm-4:10pm	Bit-precise Reasoning with Parametric Bit-vectors	Yoni Zohar	Professor, Bar-Ilan University
4:10pm-4:30pm	Integer Reasoning Modulo Different Constants in SMT	Elizaveta Pertseva	PhD Student
4:30pm-4:50pm	Bounded Quantifiers for Finite Relations	Mudathir Mohamed	Postdoc at University of Iowa
4:50pm-5:00pm	Closing Remarks	Clark Barrett	Director of Centaur
Reception
5:00pm-7:00pm	Reception