POPL 2023 (series) / CPP 2023 (series) / CPP 2023 /
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
We formalize a multivariate quantifier elimination (QE) algorithm in the theorem prover Isabelle/HOL. Our algorithm is complete, in that it is able to reduce \textit{any} quantified formula in the first-order logic of real arithmetic to a logically equivalent quantifier-free formula. The algorithm we formalize is a hybrid mixture of Tarski’s original QE algorithm and the Ben-Or, Kozen, and Reif algorithm, and it is the first complete multivariate QE algorithm formalized in Isabelle/HOL.
Mon 16 JanDisplayed time zone: Eastern Time (US & Canada) change
Mon 16 Jan
Displayed time zone: Eastern Time (US & Canada) change
14:00 - 15:30 | |||
14:00 22mTalk | A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL CPP Katherine Kosaian Carnegie Mellon University, Yong Kiam Tan Carnegie Mellon University, André Platzer Karlsruhe Institute of Technology | ||
14:22 22mTalk | P4Cub: A Little Language for Big Routers CPP Rudy Peterson Cornell University, Eric Campbell Cornell University, John Chen Cornell University, Natalie Isak Microsoft, Calvin Shyu Cornell University, Ryan Doenges Cornell University, Parsia Ataei Cornell University, Nate Foster Cornell University | ||
14:45 22mTalk | ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER CPP Haobin Ni Cornell University, Antoine Delignat-Lavaud Microsoft Research, n.n., Cédric Fournet Microsoft Research, Tahina Ramananandro Microsoft Research, Nikhil Swamy Microsoft Research | ||
15:07 22mTalk | Verifying term graph optimizations using Isabelle/HOL CPP Brae J. Webb The University of Queensland, Ian J. Hayes The University of Queensland, Mark Utting The University of Queensland | ||