Statements in the first-order logic of real arithmetic (FOL_ℝ) that involve the "there exists" and "for all" quantifiers arise in various application domains, including the formal verification of cyber-physical systems and robot motion planning. These quantifiers are difficult for both humans and computers to handle. The best way of analyzing quantified formulas in FOL_ℝ is to reduce them to logically equivalent quantifier-free formulas, through a process known as quantifier elimination (QE). By removing the quantifiers in a logically sound manner, QE makes formulas significantly simpler to analyze (as quantifier-free formulas can be easily evaluated by arithmetic in individual states, whereas quantified formulas cannot).

Given the safety-critical nature of applications involving real quantifier elimi nation, having correct QE algorithms is crucial. For this, formally verifying QE algorithms–by implementing them in a theorem prover and developing associated proofs of correctness–is very desirable. These proofs of correctness are rigorous, as they rely only on the trusted core of the theorem prover–a (typically small) foundation of trusted code/logical axioms from which all other results are built.

This thesis provides formally verified support for real QE with a two-pronged approach: First, develop support for efficient even if incomplete QE algorithms (which are specialized to a fragment of real arithmetic), with a focus on filling gaps in the existing body of related work. Second, develop support for a promising complete QE algorithm with the potential for eventual efficiency / good complexity. For the first goal, the thesis discusses a verification of linear and quadratic virtual substitution with a focus on correctness, experimentation, and optimization; the experiments show that this verified VS implementation is competitive with unverified implementations of VS. For the second goal, the thesis discusses the verification of a complete QE algorithm that uses insights from the influential Ben-Or, Kozen, and Reif (BKR) algorithm; although this verified algorithm does not currently exploit all insights from BKR and does not yet realize practical efficiency, it lays groundwork for eventual verified complete QE algorithms with strong parallel complexity bounds. This thesis uses the theorem prover Isabelle/HOL for both verifications.

102 pages

Thesis Committee:
André Platzer (Chair)
Jeremy Avigad
Frank Pfenning
Dexter Kozen (Cornell University)
Lawrence Paulson (University of Cambridge)

Srinivasan Seshan, Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu