Formal Verification

Automatic Verification of Higher Order programs

Implements a Hoare style forward verifier for programs with higher order features.

Assertion-annotated Program Verification with Path Splitting

Propose a new framework for verifying assertion-annotated programs by analyzing control flow of Clight programs and splitting proof goals based on user-provided assertions in VST

Formal Verification of Tarjan's Algorithm

Proving Functional Correctness of Tarjan's Strongly Connected Component Algorithm and its C Implementation in Coq and VST.

Formlization of Classical Real Number Theory

Implement the definition and completeness proof of Cantor's Construction of Real Number (Cauchy's sequence of rational numbers) in Coq.