| 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 |
