Computer Science Thesis Proposal

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

Keywords:

Thesis Proposal