Computer Science Thesis Proposal

Friday, April 8, 2022 - 10:30am


In Person and Virtual - ET Traffic21 Classroom, Gates Hillman 6501 and Zoom


KATHERINE CORDWELL, Ph.D. Student Computer Science Department Carnegie Mellon University

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.
Thesis Committee:
André Platzer (Chair)
Jeremy Avigad
Frank Pfenning
Dexter Kozen (Cornell University)
Lawrence Paulson (University of Cambridge)
Additional Information

In Person and Zoom Participation. See announcement.

For More Information, Contact:


Thesis Proposal