Assertion-annotated Program Verification with Path Splitting

In this project, we propose a new framwork for verifying assertion-annotated programs, so that users can first write assertions in their C program, and then only verify the small hoare triples between assertions as separate proof goals. Our formally proved soundness theorem will link these proof goals together, ensuring correctness of the whole program.

Litao Zhou (Tony)
Litao Zhou (Tony)
Junior Bachelor Student

My research interest includes Programming Language, Functional Programming and Formal Verification.