C* Language Extends C with Integrated Verification Capabilities

Integrating Verification into C

C* is a proof-integrated language design that extends the C programming language with built-in verification capabilities. This extension is powered by a symbolic execution engine and an LCF-style proof kernel, allowing for the direct integration of formal verification into the development workflow.

Addressing Development Challenges

The primary goal of C* is to bridge the gap between programming and verification environments. Currently, conventional programmers are rarely involved in verifying their own code, leading to increased development and maintenance costs for verified software. C* addresses this by enabling programmers to embed proof-code blocks alongside implementation code, facilitating interactive updates to the proof state in real-time.

Expressive Proof Support

C* offers expressive and extensible proof support, allowing users to create reusable libraries of logical definitions, theorems, and programmable proof automation. A key aspect of C* is its use of C as the common language for both implementation and proof code development, unifying these two processes.

Evaluation and Results

A prototype of C* was implemented and evaluated using a benchmark of small C programs and a complex real-world case study: the attach function of pKVM's buddy allocator. The evaluation demonstrated that C* supports the verification of a broad range of C programming idioms and can handle complex reasoning tasks in practical scenarios.