C*: Unifying Programming and Verification in C
Summary
C*: Unifying Programming and Verification in C introduces C*, a proof-integrated extension of C that enables real-time verification by embedding proof-code blocks alongside implementation code. It uses a symbolic execution engine and an LCF-style proof kernel to unify programming and verification, with a prototype evaluated on small C programs and the attach function of pKVM's buddy allocator.