Friday, April 8, 2022 - 10:30am
Location:In Person and Virtual - ET Traffic21 Classroom, Gates Hillman 6501 and Zoom
Speaker:KATHERINE CORDWELL, Ph.D. Student Computer Science Department Carnegie Mellon University http://www.cs.cmu.edu/~kcordwel
Formalizing Algorithms for Real Quantifier Elimination
This thesis will focus on the dearth of efficient formally verified support for algorithms for real quantifier elimination. It proposes a two-pronged approach: first, verify a general-purpose multivariate QE algorithm based on the Ben-Or, Kozen, and Reif decision procedure and its variant by Renegar; second, verify a suite of highly efficient but limited QE methods, particularly virtual substitution, on top of the general-purpose algorithm.
André Platzer (Chair)
Dexter Kozen (Cornell University)
Lawrence Paulson (University of Cambridge)
In Person and Zoom Participation. See announcement.