C*: Unifying Programming and Verification in C

# Unifying Programming and Verification in C
Source: [https://arxiv.org/html/2504.02246](https://arxiv.org/html/2504.02246)
DOI:[XXXXXXX\.XXXXXXX](https://doi.org/XXXXXXX.XXXXXXX)Conference:Make sure to enter the correct conference title from your rights confirmation emai; June 03–05, 2018; Woodstock, NYISBN:978\-1\-4503\-XXXX\-X/18/06,Jiayi ZhuangAffiliation:Peking University,Beijing,China,Houjin ChenAffiliation:Peking University,Beijing,China,Jinkai FanAffiliation:Peking University,Beijing,China,Wenbo XuAffiliation:Peking University,Beijing,China,Zhiyi WangAffiliation:Peking University,Beijing,China,Di WangAffiliation:Peking University,Beijing,China,Qinxiang CaoAffiliation:Shanghai Jiao Tong University,Shanghai,China,Yingfei XiongAffiliation:Peking University,Beijing,China,Haiyan ZhaoAffiliation:Peking University,Beijing,ChinaandZhenjiang HuAffiliation:Peking University,Beijing,China

Received 5 June 2009

###### Abstract\.

Ensuring the correct functionality of systems software, given its safety\-critical and low\-level nature, is a primary focus in formal verification research and applications\. Despite advances in verification tooling, conventional programmers are rarely involved in the verification of their own code, resulting in higher development and maintenance costs for verified software\. A key barrier to programmer participation in verification practices is the disconnect of environments and paradigms between programming and verification practices, which limits accessibility and real\-time verification\.

We introduceC⋆\\star, a proof\-integrated language design for C programming\.C⋆\\starextends C with verification capabilities, powered by a symbolic execution engine and an LCF\-style proof kernel\. It enables real\-time verification by allowing programmers to embed proof\-code blocks alongside implementation code, facilitating interactive updates to the current proof state\. Its expressive and extensible proof support allows users to build reusable libraries of logical definitions, theorems, and programmable proof automation\. Crucially,C⋆\\starunifies implementation and proof code development by using C as the common language\.

We implemented a prototype ofC⋆\\starand evaluated it on a representative benchmark of small C programs and a challenging real\-world case study: theattachfunction of pKVM’s buddy allocator\. Our results demonstrate thatC⋆\\starsupports the verification of a broad subset of C programming idioms and effectively handles complex reasoning tasks in real\-world scenarios\.

###### Keywords:

software verification, real\-time verification, C programming, LCF\-style theorem proving, separation logic, symbolic execution

## 1\.Introduction

#### Background

Systems software forms the infrastructure of modern computing, providing the low\-level foundation on which all higher\-level applications operate\. Given its critical role, recent years have seen considerable advances in the formal verification of systems software components\([Leinenbach and Santen, 2009](https://arxiv.org/html/2504.02246#bib.bib26);[Tao et al\., 2021](https://arxiv.org/html/2504.02246#bib.bib41);[Li et al\., 2021](https://arxiv.org/html/2504.02246#bib.bib28);[Klein et al\., 2014](https://arxiv.org/html/2504.02246#bib.bib23);[Xu et al\., 2016](https://arxiv.org/html/2504.02246#bib.bib42);[Gu et al\., 2016](https://arxiv.org/html/2504.02246#bib.bib17);[Amani et al\., 2016](https://arxiv.org/html/2504.02246#bib.bib3);[Chen et al\., 2015](https://arxiv.org/html/2504.02246#bib.bib9);[Leroy, 2009](https://arxiv.org/html/2504.02246#bib.bib27);[Kumar et al\., 2014](https://arxiv.org/html/2504.02246#bib.bib25);[Protzenko et al\., 2020](https://arxiv.org/html/2504.02246#bib.bib34);[Ramananandro et al\., 2019](https://arxiv.org/html/2504.02246#bib.bib37)\)\.

In this paper, we focus on the verification of software implemented in the C programming language, which remains widely used due to its predictable performance, fine\-grained control over system resources, and the vast amount of existing critical code written in it\. Significant progress has been made in verification frameworks and toolchains for C programs\([Greenaway et al\., 2014](https://arxiv.org/html/2504.02246#bib.bib15);[Zhou et al\., 2024](https://arxiv.org/html/2504.02246#bib.bib43);[Mansky and Du, 2024](https://arxiv.org/html/2504.02246#bib.bib29);[Leroy, 2009](https://arxiv.org/html/2504.02246#bib.bib27);[Appel, 2011](https://arxiv.org/html/2504.02246#bib.bib4);[Sammler et al\., 2021](https://arxiv.org/html/2504.02246#bib.bib40);[Pulte et al\., 2023](https://arxiv.org/html/2504.02246#bib.bib36);[Jacobs et al\., 2011](https://arxiv.org/html/2504.02246#bib.bib21);[Gruetter et al\., 2024](https://arxiv.org/html/2504.02246#bib.bib16);[Kirchner et al\., 2015](https://arxiv.org/html/2504.02246#bib.bib22);[Cohen et al\., 2009](https://arxiv.org/html/2504.02246#bib.bib10);[Protzenko et al\., 2017](https://arxiv.org/html/2504.02246#bib.bib35)\)\. The substantial progress in the development of formally verified software components and verification tools has demonstrated the feasibility of large\-scale verification, and has brought us closer to the vision where all critical software should be verified\([Hoare et al\., 2009](https://arxiv.org/html/2504.02246#bib.bib20)\)\.

Despite these successes, formally verified software projects remain costly, in the sense that they require specialized teams with significant expertise, and usually need person\-years to complete\([Leroy, 2009](https://arxiv.org/html/2504.02246#bib.bib27);[Klein et al\., 2014](https://arxiv.org/html/2504.02246#bib.bib23)\)\. For the wider adoption of verification practices, the development and maintenance costs for verified software must be reduced\. One significant source of the high costs arises from the*lack of involvement from programmers*, who carry out most of the implementation work yet rarely participate in the verification of their own code\.

#### Existing approaches

One reason for the lack of programmer involvement is that the verification of C programs typically requires an external environment, e\.g\., an interactive theorem prover such as Coq, which demands programmers to learn a significantly different proving paradigm from the C programming experience\. Examples in this category include AutoCorres\([Greenaway et al\., 2012](https://arxiv.org/html/2504.02246#bib.bib14)\), VST\([Appel, 2011](https://arxiv.org/html/2504.02246#bib.bib4)\)and its recent variant in Iris\([Mansky and Du, 2024](https://arxiv.org/html/2504.02246#bib.bib29)\), as well as the Live Verification framework\([Gruetter et al\., 2024](https://arxiv.org/html/2504.02246#bib.bib16)\)\. The first three translate existing C programs into certain logical representations in the meta\-logic \(a monadic shallow embedding or a deep embedding\) and then require programmers to conduct proofs around these representations in their underlying theorem prover\. The Live Verification framework chooses another approach by composing the program lazily and incrementally along the proof process, relying on the specific mechanism of existential meta\-variables in Coq to represent a partially constructed program\.

To encourage more involvement from programmers, other C verification tools provide language\-level integration of programming and verification to make the verification process more accessible to programmers\. There are two main categories: \(i\)*assertion\-based verifiers*such as Frama\-C\([Kirchner et al\., 2015](https://arxiv.org/html/2504.02246#bib.bib22)\)and VST\-A\([Zhou et al\., 2024](https://arxiv.org/html/2504.02246#bib.bib43)\), and \(ii\)*advanced\-type\-based verifiers*such as RefinedC\([Sammler et al\., 2021](https://arxiv.org/html/2504.02246#bib.bib40)\)and CN\([Pulte et al\., 2023](https://arxiv.org/html/2504.02246#bib.bib36)\)\. These tools allow programmers to annotate a C program with intermediate assertions \(e\.g\., loop invariants\) or advanced types \(e\.g\., ownership and refinement types\) apart from the specifications to guide the verification process\. These tools are usually*\(semi\-\)automated*, in the sense that they employ an assertion or type checker to automatically verify if the program conforms to the specifications with the help of the programmer\-provided annotations\. However, when automation falls short, programmers again need to switch to an external theorem proving environment to complete the verification \(e\.g\., in Coq\([Zhou et al\., 2024](https://arxiv.org/html/2504.02246#bib.bib43);[Sammler et al\., 2021](https://arxiv.org/html/2504.02246#bib.bib40);[Pulte et al\., 2023](https://arxiv.org/html/2504.02246#bib.bib36)\)\)\. To mitigate the issue, VeriFast\([Jacobs et al\., 2011](https://arxiv.org/html/2504.02246#bib.bib21)\)—an assertion\-based automated verifier for C programs—provides limited proof support such that programmers can annotate the program with a fixed set of proof commands and write ghost lemma functions to perform certain forms of inductive reasoning\. However, VeriFast lacks the expressiveness and extensibility in proof support required for the collaborative verification of low\-level systems software between programmers and proof experts\.

#### Our goal

As discussed above, there is no satisfactory verification tooling for conventional systems programmers\. In this paper, we aim to design and implement a new C verification tool that satisfies the following two criteria:

- •it should provide*language\-level integration*of programming and verification; and
- •it should provide*comprehensive proving capabilities*within C’s programming paradigm\.

To further enhance the usability of the C verification tool, we consider one more criterion:

- •it should provide support for*real\-time verification*, i\.e\., the tool should be able to provide a static summary of the program state at every program point and allow programmers to inspect every intermediate proof state inside a proof\.

#### Our approach

In this paper, we proposeC⋆\\star, a proof\-integrated language that embeds full\-fledged verification and proving capabilities in C\. We highlight the three key designs ofC⋆\\starbelow\.

- •We adapt the assertion\-based design by allowing programmers to annotate a program with*separation\-logic*assertions and incorporating*forward symbolic execution*, which abstracts the complexities of concrete semantics and maintains a static summary of the symbolic program state after processing a program fragment\.
- •We integrate the C programming language with*LCF\-style proof support*for*higher\-order logic*, which provides a comprehensive and extensible interface for programming formal proofs and transforming symbolic states, facilitating the development of high\-level reasoning abstractions—as*proof support libraries*—using the full power of C\.
- •With the previous two designs,C⋆\\staris ready to support real\-time verification: forward symbolic execution provides a summary of the symbolic program state at every program point, and the LCF\-style proof support allows programmers to inspect and manipulate the proof state using the familiar programming constructs of C\.

We implemented a prototype ofC⋆\\starand evaluated it on a suite of C programs to demonstrateC⋆\\star’s practicality for the development of verified programs\. Specifically, our evaluation shows thatC⋆\\star\(i\) supports systems programming idioms and a large subset of C language features, \(ii\) provides sufficient expressiveness for advanced ownership and functional reasoning, and \(iii\) is capable of verifying realistic C programs\.

#### Contributions

In this paper, we make the following contributions:

- •We propose a proof\-integrated language design that embeds specifications and proof code in C programs, provides comprehensive reasoning capabilities within C’s programming paradigm, and thus make formal verification practices accessible to programmers\.
- •We implemented our design as theC⋆\\startoolchain by extending C with two well\-established components: a symbolic\-execution engine and an LCF\-style proof kernel, interfacing both to create a lightweight yet powerful verification workflow\.
- •We evaluated our implementation ofC⋆\\staron a suite of benchmark programs from the literature and a realistic case study to show it is effective in developing verified C programs with the help ofC⋆\\star’s standard proof\-support library\.

## 2\.A Guided Tour ofC⋆\\star

In this section, we present a guided tour for developing a verified C program inC⋆\\star\. We take theclearfunction shown inas the running example, whose desired functionality is to resetlencontiguous bytes that start from a base addressto\. The implementation code ofclearconsists of lines 3, 6, 8, 10, 17, 19, 20, 22, and 24; others are verification\-specific code\. In the implementation code, the programmer declares a local variableiin line 8, followed by a loop from line 10 to line 22, where each loop iteration sets thei\-th byte from the base addresstoto zero and incrementsiby one untilireaches the function parameterlen\.

We explain the verification\-specific code in a way that guides the reader through the incremental development process followingC⋆\\star’s workflow\. Our explanation will follow the three criteria mentioned in[section1](https://arxiv.org/html/2504.02246#S1):[section2\.1](https://arxiv.org/html/2504.02246#S2.SS1)for language\-level integration of programming and verification, e\.g\., how the user writes specifications and assertions aboutclear;[section2\.2](https://arxiv.org/html/2504.02246#S2.SS2)for comprehensive proving capabilities via C programming, e\.g\., how the user proves the implementation ofclearcomforms to its specification; and[section2\.3](https://arxiv.org/html/2504.02246#S2.SS3)for real\-time program verification, e\.g\., howC⋆\\staraids the user during the incremental development\.

1\#include"cstarlib\.h"

2\#include"clear\.h"

3voidclear\(void\*to,intlen\)

4\[\[require\(‘fact\(len\>=0\)\*\*undef\_array\_at\(to,Tchar,len\)‘\)\]\]

5\[\[ensure\(‘array\_at\(to,Tchar,replicate\(len,0\)\)‘\)\]\]

6\{

7«termparams=‘data\_at\(&"to",Tptr,to\)\*\*data\_at\(&"len",Tint,len\)‘;»

8inti=0;

9«»

10while\(i<len\)

11\[\[invariant\(‘∃\\exists\(i:integer\)\.

12fact\(0<=i&&i<=len\)\*\*

13data\_at\(&"i",Tint,i\)\*\*$\{params:hprop\}\*\*

14array\_at\(to,Tchar,replicate\(i,0\)\)\*\*

15undef\_array\_at\(to\+i\*sizeof\(Tchar\),Tchar,len\-i\)

16‘\)\]\]

17\{

18«single\_out\_location\(\);»

19\*\(\(char\*\)to\+i\)=\(char\)0;

20i=i\+1;

21«»

22\}

23«»

24\}

Listing 1:An example verified C program inC⋆\\star\.### 2\.1\.Language\-level Integration of Programming and Verification

The first thing to do for verifying a program is correct is to*specify*how it is supposed to be correct\. It is a common practice to specify a function’s expected behavior by formulating its*pre\-*and*post\-*conditions, i\.e\., the expected program states before calling the function and after returning from it\. For the desired functionality ofclear, the pre\-condition could be that the function parameterlenis non\-negative and the other parametertois a base address that points to a memory chunk of at leastlencontiguous bytes\. The corresponding post\-condition would be thatlencontiguous bytes starting from the addresstoare set to zero\. To formally formulate such conditions for low\-level heap\-manipulating programs such asclear, we adapt*separation logic*inC⋆\\star’s design\.

###### Background 0 \(Separation Logic\)\.

The development of separation logic\([O’Hearn, 2019](https://arxiv.org/html/2504.02246#bib.bib32);[Reynolds, 2002](https://arxiv.org/html/2504.02246#bib.bib38)\)is driven by the desire to verify heap\-manipulating low\-level programs in a modular manner, especially for handling the flexibility of aliasing\. Its most salient features are \(i\) the introduction of a logical connective,*separating conjunction*, expressing non\-aliasing properties between heap fragments in a succinct way, and \(ii\) a characterizing program proof rule,*frame rule*, extending the*program locality*of Hoare logic rules with*spatial locality*when reasoning about heap\-manipulating programs\.

[Tab\.1](https://arxiv.org/html/2504.02246#S2.T1)lists the concrete notations for some separation\-logic predicates used inC⋆\\star\. The standard proof\-support library ofC⋆\\starprovides some other widely\-used predicates for program verification tasks\. For example,array\_at\(p,ty,lst\)represents a consecutive array of elements of C typetystarting at the addressp, where thenn\-th element of the array is represented by thenn\-th element in the logic\-level listlst\. Another exampleundef\_array\_at\(p,ty,len\)represents an array starting at addresspwithlenundefined values, each of which is uninitialized or irrelevant to the verification\. With separation logic, the user can specify the pre\- and post\-conditions in lines 4 and 5, respectively:

- •C⋆\\staruses the C attribute syntax\[\[require\]\]111In actual code, all the attributes are prefixed with the\[\[cstar::\]\]namespace for disambiguation\.to enclose a pre\-condition\. In line 4, the predicatefact\(len\>=0\)represents an*empty*heap with the condition thatlenis non\-negative\. The predicateundef\_array\_at\(to,Tchar,len\)represents a memory chunk oflencontinuous bytes, whereTcharis the logic\-level representation of the C typechar\. Using separating conjunction\*\*to compose the two predicates yields a precise formulation of the intended pre\-condition\.
- •C⋆\\staruses\[\[ensure\]\]for post\-conditions\. In line 5, the predicatearray\_at\(to,Tchar,replicate\(len,0\)\)represents a memory chunk oflencontinuous zeros, where the logic\-level termreplicate\(len,0\)creates a list oflenzeros\. This, again, precisely corresponds to the intended post\-condition we discussed earlier\.

Table 1\.Concrete notations for some separation\-logic predicates used inC⋆\\star\.Readers may have noticed the uses of*quotations*‘\.\.\.‘inside pre\- and post\-conditions\. The quotation mechanism allows the user to construct separation\-logic predicates and other logic\-level terms using conventional concrete syntax, which is similar to existing assertion\-based C verifiers\. But as we will show in[section2\.2](https://arxiv.org/html/2504.02246#S2.SS2), these terms are*first\-class*values inC⋆\\star: beyond being directly written with quotations, they can be computed from expressions, stored in variables, passed as arguments, and manipulated using the full capabilities of the C programming language\. This is one key difference betweenC⋆\\starand traditional assertion\-based C verifiers\.

Writing pre\- and post\-conditions is far from completing the verification, because it is generally intractable to have an algorithm to automatically verify the function body “transforms” the pre\-condition to the post\-condition\. Similar to many existing C verifiers,C⋆\\staradapts the assertion\-based design to enable a*declarative*style of verification:

###### Principle 0 \(Declarative Style of Verification\)\.

The user annotates the program with separation\-logic assertions about the expected program states that hold at specific program points\.

A particular important class of assertions are*loop invariants*\.C⋆\\staralso uses the C attribute\[\[invariant\]\]to accompany a loop with its invariant, i\.e\., a separation\-logic predicate that is expected to hold at the beginning of each loop iteration\. Lines 11–16 specify the loop invariant, which intuitively states that at thei\-th iteration, the value ofishould be between zero andlen\(line 12\), local variables and parameters are stored properly in the memory withTintbeing the logic\-level representation of the C typeint\(line 13\), and the base addresstopoints to a memory chunk that starts withizeros \(line 14\) followed bylen\-iunspecified bytes \(line 15\)\. Note that in line 13 the code uses an*anti\-quotation*$\{params:hprop\}to interpolate a predicate defined in line 7\. This again indicates that predicates are first\-class values and we defer the discussion of anti\-quotations to[section2\.2](https://arxiv.org/html/2504.02246#S2.SS2)\.

With extra assertions including invariants, an assertion\-based verifier usually splits the verification into multiple sub\-tasks, each of which corresponds to prove a Hoare triple for a*straight\-line*program segment\. For example, to verify that theclear’s implementation code conforms to the pre\- and post\-conditions, it is sufficient to complete three sub\-tasks \(i\.e\., verifying three Hoare triples\):

- •prove the code in line 8 transforms the pre\-condition to the loop invariant \(line 9\);
- •prove that the loop body \(lines 19 and 20\) re\-establishes the loop invariant \(line 21\); and
- •prove that the loop invariant—with the loop condition \(in line 10\) being false—entails the post\-condition \(line 23\)\.

Each sub\-task, i\.e\., the proof of each Hoare triple\{P\}​S​\{Q\}\\\{~P~\\\}~S~\\\{~Q~\\\}, involves two parts: \(i\) reasoning about semantics of the programSS, i\.e\., finding the strongest post\-conditionQ𝗌𝗉Q\_\{\\mathsf\{sp\}\}ofSSw\.r\.t\. the pre\-conditionPP, and \(ii\) carrying out an entailment proof, i\.e\., proving thatQ𝗌𝗉Q\_\{\\mathsf\{sp\}\}entailsQQ\. Instead of employing automated provers for both parts—as many other assertion\-based verifiers do—C⋆\\staradapts a*predictable*mechanism of automation by integrating*forward symbolic execution*to reason about program semantics, i\.e\., part \(i\) of each verification sub\-task\.

###### Background 0 \(Forward Symbolic Execution\)\.

Since the work of Berdine et al\.\([Berdine et al\., 2005](https://arxiv.org/html/2504.02246#bib.bib5)\), separation logic has been effectively used as a sound foundation for forward symbolic execution, which closely matches a programmer’s operational intuition about the effects of statements on program states, while abstracting away concrete semantic details\. It achieves this by providing a highly predictable algorithm for automatically applying structural program logic rules for separation\-logic predicates in suitable forms, i\.e\., the*symbolic heap*fragment of separation logic\([Cao et al\., 2018](https://arxiv.org/html/2504.02246#bib.bib6)\)\.

Using a symbolic\-execution engine,C⋆\\starcomputes a*symbolic state*for each program point\. The symbolic state consists of the values of the program variables and the view of the heap fragments that are worked on and owned by the program\. For example, at the beginning of the function body ofclear\(in line 6\), symbolic execution uses the pre\-condition annotated in line 4 to initialize the symbolic state to be the same as the following separation\-logic predicate, which additionally consists ofdata\_atpredicates for the function parameters:

fact\(len\>=0\)\*\*undef\_array\_at\(to,Tchar,len\)\*\*

data\_at\(&"to",Tptr,to\)\*\*data\_at\(&"len",Tint,len\)

HereTptris the logic\-level representation of C’s pointer types\.

If symbolic execution were always successful, the remaining proof obligations for the user would all be separation\-logic entailments, i\.e\., part \(ii\) of each verification sub\-task\. In[section2\.2](https://arxiv.org/html/2504.02246#S2.SS2), we will showC⋆\\star’s capabilties in supporting the user to develop the logical proofs\. On the other hand, unfortunately, the price of having a predictable symbolic\-execution engine is that it will not try to automate the reasoning and transformations on the symbolic state that a user might find intuitive to perform\. For example, in line 19, the statement assigns to the address\(\(char\*\)to\+i\), but the symbolic state—the loop invariant in this case—does not explicitly describe the memory cell pointed by the address\. As a result,C⋆\\star’s symbolic\-execution engine cannot \(yet\) automatically process the assignment\. In[section2\.2](https://arxiv.org/html/2504.02246#S2.SS2), nevertheless, we will show howC⋆\\star’s proving capabilities provide an*operational*style of verification, where users can convey and formalize their high\-level intuitive ideas on manipulating the symbolic state\.

### 2\.2\.Comprehensive Proving Capabilities via C Programming

As discussed in[section2\.1](https://arxiv.org/html/2504.02246#S2.SS1),C⋆\\star’s proving capabilities should support its users in the following two tasks:

- •developing logical proofs for entailments, and
- •manipulating symbolic states inside the implementation code\.

In particular,C⋆\\star’s support should satisfy a key criterion:

- •allow the user to*programmably*develop logical proofs and manipulate symbolic states, using C’s conventional programming constructs\.

To achieve the aforementioned goals, we adapt*LCF\-style theorem proving*inC⋆\\star\.

###### Background 0 \(LCF\-style Theorem Proving\)\.

The LCF architecture is a general technique for embedding formal logics into a programming language\. Pioneered by Robin Milner and colleagues in the early work on the Edinburgh LCF theorem prover\([Gordon, 2000](https://arxiv.org/html/2504.02246#bib.bib13);[Harrison et al\., 2014](https://arxiv.org/html/2504.02246#bib.bib19)\), its descendants are still widely used today\([Harrison, 2009](https://arxiv.org/html/2504.02246#bib.bib18);[Nipkow et al\., 2002](https://arxiv.org/html/2504.02246#bib.bib31)\)\. In LCF\-style provers, a general\-purpose programming language is used as the*meta\-language*to implement*object logic*entities such as*terms*,*types*, and*theorems*\. These are represented as recursive data structures, making formal proof a*programming*process of constructing theorems from a set of axioms using primitive inference rules\. Specifically, the axioms are encoded as constants, and the inference rules are implemented as functions that take premises and return conclusions as theorems if the rules can be successfully instantiated\.

InC⋆\\star, we integrate an LCF\-style proof kernel with*higher\-order logic*as the object logic\. The kernel is wrapped by a C interface; in other words, the meta\-language inC⋆\\star’s design is the standard C programming language\. To distinguish the code for developing logical proofs and manipulating symbolic states from ordinary implementation code,C⋆\\starintroduces*proof\-code blocks*delimited by the «\.\.\.» syntax\.222In actual code, we use the\[\[cstar::proof\(\.\.\.\)\]\]attribute to embed proof\-code blocks\.Arbitrary C code is allowed in proof\-code blocks, with the ability to introduce bindings and construct values of typetermandthm, corresponding to object\-logic terms and theorems, respectively\. Recall that we mentioned that inC⋆\\star, separation\-logic predicates are first\-class values\. Indeed, they are justtermvalues of object\-logic typehprop\(short for heap propositions\)\. The quotation and anti\-quotation mechanisms are thereby introduced to conveniently constructtermvalues\. For example, in line 7 of, the code stores thedata\_atpredicates regarding ownership of the parameters—wrapped by a quotation‘\.\.\.‘—in a variable calledparams\. In the following proof\-code blocks and assertions \(e\.g\., invariants\), the user can useparamsas if it is a normal program variable\.333All proof blocks in a function body are in the same scope, and global proof\-code blocks \(that is outside of any function body\) are file\-scoped\. Local scopes can be created using C blocks\\\{\.\.\.\\\}\. See[section4\.1](https://arxiv.org/html/2504.02246#S4.SS1)for more details\.In line 13, the code indeed uses it; combined with the anti\-quotation$\{params:hprop\}, it reduces redundancy when writing the loop invariant\.

Because separation\-logic predicates are just values inC⋆\\star, it becomes natural to write C code to manipulate symbolic states, which are special kinds of separation\-logic predicates\. Such capability ofC⋆\\starenables an*operational*style of verification:

###### Principle 0 \(Operational Style of Verification\)\.

The user manipulates the symbolic state using arbitrary C code, provided they can give justifications, i\.e\., theorems for the corresponding separation\-logic entailments, for the manipulations they made\.

For example, the operational style of verification is applied in line 18\. Here, the symbolic state—computed by the symbolic\-execution engine—is equivalent to the following predicate:

∃\\exists\(i:integer\)\.fact\(i<len\)\*\*fact\(0<=i&&i<=len\)\*\*

data\_at\(&"i",Tint,i\)\*\*data\_at\(&"to",Tptr,to\)\*\*data\_at\(&"len",Tint,len\)\*\*

array\_at\(to,Tchar,replicate\(i,0\)\)\*\*undef\_array\_at\(to\+i\*sizeof\(Tchar\),Tchar,len\-i\)

As discussed above about symbolic execution, symbolically executing the next statement \(in line 19\) would fail, because the symbolic state does not explicitly describe the address\(\(char\*\)to\+i\)\. Intuitively, the user should “transform” the symbolic state to some form containingundef\_data\_at\(to\+i\*sizeof\(Tchar\),Tchar\)as a separating conjunct, which represents the ownership of the memory location being stored into\. By inspecting the symbolic state, the user can see that a transformation of the view of the heap is needed to satisfy the requirement: by splitting theundef\_array\_atpredicate into the separating conjunction of its head element \(as anundef\_data\_atpredicate\) and the rest of the slice \(as anundef\_array\_atpredicate with smaller length and starting at a bigger offset\)\. The split is valid due to the fact thati<lenholds in current state, which entails the factlen\-i\>0, meaning the slice is non\-empty\. The corresponding justification—as proof code—for this intuitive transformation is wrapped in the proof proceduresingle\_out\_location\.

The implementation of the proof proceduresingle\_out\_locationis shown in\. It demonstrates howC⋆\\starallows proving separation\-logic entailments using conventional C programming constructs and high\-level derived rules from the proof\-support libraries, making the intuitive reasoning process easy to implement as proof code\. Thanks to the LCF\-style design, logical rules are just C functions that returnthmvalues, which represent proven theorems\.

- •*Derive the transformation rule \(lines 2–7\)\.*Theundef\_array\_at\_select\_firsttheorem, from the proof\-support libraryclear\.hincluded by theC⋆\\starprogram in, asserts that for any uninitialized array, we can single out the first element and treat the remainder as another uninitialized array, provided the length of the array is greater than zero\. The resulting theorem from this derived\-rule application is shown by the comment in lines 4–7, where==\>denotes standard logical implication and\|\-\-denotes separation\-logic entailment\.
- •*Rewrite using linear arithmetic facts \(lines 8–14\)\.*Therewrite\_rule\_listfunction—from the standard proof\-support librarycstarlib\.h—takes anNULL\-terminated array of equational theorems and another theorem, and rewrites the second argument using the equational theorems\. It is used here to rewrite the theorem using linear arithmetic facts, which are derived automatically by calling thearith\_rulefunction, to align with the predicates in the current symbolic state\. The array\-destructing theoremundef\_array\_at\_destructis re\-assigned to the rewritten theorem by the statement in line 13\.
- •*Perform local transformation with frame inferred from the symbolic state \(lines 15–17\)\.*Thelocal\_applyfunction is an important derived rule incstarlib\.h\. It allows programmers to perform a local transformation with the frame being inferred from the symbolic state\. Specifically, it takes two arguments: the current symbolic state and a local\-transformation theorem\. In line 15, we fetch the current symbolic state using the built\-inget\_symbolic\_statefunction, and use thelocal\_applyfunction to perform a local transformation justified by the theoremdest\_undef\_array\. The result of the transformation is then put back to the symbolic\-execution engine using the built\-inset\_symbolic\_statefunction in line 17\.

1voidsingle\_out\_location\(void\)\{

2thmdest\_undef\_array=

3undef\_array\_at\_select\_first\(‘to\+i\*sizeof\(Tchar\)‘,‘Tchar‘,‘len\-i‘\);

4

5undef\_array\_at\(to\+i\*sizeof\(Tchar\),Tchar,len\-i\)\|\-\-

6undef\_data\_at\(to\+i\*sizeof\(Tchar\),Tchar\)\*\*

7undef\_array\_at\(\(to\+i\*sizeof\(Tchar\)\)\+sizeof\(Tchar\),Tchar,len\-i\-1\)\*/

8thmarith\_facts\[\]=\{

9arith\_rule\(‘len\-i\>0<=\>i<len‘\),

10arith\_rule\(‘len\-i\-1==len\-\(i\+1\)‘\),

11arith\_rule\(‘\(to\+i\*sizeof\(Tchar\)\)\+sizeof\(Tchar\)==

12to\+\(i\+1\)\*sizeof\(Tchar\)‘\),NULL\};

13dest\_undef\_array=rewrite\_rule\_list\(arith\_facts,dest\_undef\_array\);

14

15thmfinal\_thm=local\_apply\(get\_symbolic\_state\(\),dest\_undef\_array\);

16

17set\_symbolic\_state\(final\_thm\);

18\}

Listing 2:Proof procedure: single out the first element of the uninitialized slice\.
### 2\.3\.Real\-time Program Verification

In the previous two sections, we used the verification of the functionclearto illustrate \(i\) howC⋆\\starincorporates separation logic and forward symbolic execution to provide language\-level integration of programming and verification, as well as \(ii\) howC⋆\\starintegrates LCF\-style proof support for higher\-order logic to provide comprehensive proving capabilities within C’s programming paradigm\. In particular, separation\-logic predicates are first\-class values and proof\-code blocks can manipulate symbolic states and proof states\.

We claim thatC⋆\\starachieves*real\-time*program verification, i\.e\., the user can carry out verification as they program the implementation code incrementally\. It achieves this goal by orchestrating the symbolic\-execution engine and the LCF\-style proof kernel together, creating a*proof\-supporting runtime*that runs proof\-code blocks and symbolic execution of program segments in an*interleaving*manner, and provides the symbolic state at every program point in implementation code as well as the proof state in proof\-code blocks\.

Firstly,C⋆\\staris capable of providing the symbolic state at every program point, given that \(i\) every function has pre\- and post\-conditions, \(ii\) every loop has an invariant, and \(iii\) the required maps\-to predicates are present in the symbolic state before executing a primitive statement\. This is achieved by a combination of forward symbolic execution for separation logic and the ability to write proof\-code blocks to manipulate the symbolic state\. The symbolic state in the symbolic\-execution engine is always represented as a separation\-logic assertion in a canonical form, known as*symbolic heaps*\([Berdine et al\., 2005](https://arxiv.org/html/2504.02246#bib.bib5)\)\. When a statement \(e\.g\., an assignment\) is symbolically executed, the symbolic\-execution engine requires the primitive maps\-to predicate \(i\.e\.,data\_atorundef\_data\_at\) for the accessed memory locations be present in the current symbolic heap as a separating conjunct; if so, the engine modifies the symbolic heap locally\([Jacobs et al\., 2011](https://arxiv.org/html/2504.02246#bib.bib21)\)\. For example, when executing the store statement\*\(\(char\*\)to\+i\)=\(char\)0in line 19 of, the symbolic\-execution engine confirms that the current symbolic heap contains the assertion‘undef\_data\_at\(to\+i\*sizeof\(Tchar\),Tchar\)‘, representing the ownership of the memory location being stored into, and then substitutes the predicate with‘data\_at\(to\+i\*sizeof\(Tchar\),Tchar,0\)‘, reflecting the effect of the store statement\. The other predicates in the symbolic heap are left unchanged, being justified by the frame rule of separation logic\. It is worth noting that for the symbolic\-execution engine to achieve this,C⋆\\starneeds to first execute the proof\-code block in line 18 ofto transform the symbolic heap accordingly, before symbolically executing the store statement\.

Secondly,C⋆\\star’s runtime environment for running proof\-code blocks is capable of providing the proof state in proof\-code blocks\. The proof state records the concrete values oftermandthmvariables declared in proof\-code blocks, as well as proof functions and theorems included from proof\-support libraries\. For example, when a user is developing the functionclearand writes down line 18 ofto callsingle\_out\_location, the environment of the proof\-supporting runtime should be able to find the function definition ofsingle\_out\_locationin\. This ability comes from the LCF\-style theorem proving, where proofs are ordinary programs that manipulate terms and theorems\. Thus,C⋆\\starcan assemble all the proof\-code blocks inside a function and its dependent proof\-support functions together as a C program, compile it, and execute it to record the concrete values of variables\.

## 3\.Core Design

In this section, we present the core design ofC⋆\\starfrom two perspectives\. Following the discussion in[section2\.3](https://arxiv.org/html/2504.02246#S2.SS3), we explainC⋆\\star’s internal mechanisms from the developer’s perspective in[section3\.1](https://arxiv.org/html/2504.02246#S3.SS1), i\.e\.,C⋆\\star’s verification\-specific workflow and its proof\-supporting runtime\. Following the guided tour in[sections2\.1](https://arxiv.org/html/2504.02246#S2.SS1)and[2\.2](https://arxiv.org/html/2504.02246#S2.SS2), we describeC⋆\\star’s language features from the user’s perspective in[section3\.2](https://arxiv.org/html/2504.02246#S3.SS2), i\.e\.,C⋆\\star’s verification\-specific interface and its proving capabilities\.

### 3\.1\.Workflow ofC⋆\\starToolchain

Figure 1\.The ideal workflow ofC⋆\\star’s proof\-checking phase\.TheC⋆\\startoolchain consists of three components: theC⋆\\starcompiler, the LCF\-style proof kernel, and the symbolic\-execution engine\. The interaction between these components during the*proof\-checking phase*of aC⋆\\starprogram is illustrated conceptually in[Fig\.1](https://arxiv.org/html/2504.02246#S3.F1)\. After proof checking, the*deployment phase*becomes straightforward: because all verification\-specific annotations are wrapped in C attributes, the verified program can be compiled directly with C compilers such asgccorclang\.

The proof\-checking phase of aC⋆\\starprogram can be summarized as a three\-stage process: the*translation stage*, the*operational proof checking stage*, and the*residual proof checking stage*\.

#### Translation stage\.

In the first stage, theC⋆\\starcompiler processes the inputC⋆\\starprogram, and produces an*operational proof program*\. The inputC⋆\\starprogram consists of three main components: \(i\) implementation code, \(ii\) verification annotations including specifications \(e\.g\.,\[\[require\]\]and\[\[ensure\]\]attributes\) and intermediate assertions \(e\.g\.,\[\[invariant\]\]attributes\), and \(iii\) embedded proof\-code blocks\. During translation, theC⋆\\starcompiler combines part \(i\) and part \(ii\) to form the annotated C code, slices it into segments that are separated by proof\-code blocks, and stores the segments as serializable data structures in the proof code\. For part \(iii\), i\.e\., the proof\-code blocks, theC⋆\\starcompiler assembles them into the main code for execution\. The compiler also handles syntax extensions such as quotation and anti\-quotation, translating them into applications of term\-constructing functions\.[Fig\.2](https://arxiv.org/html/2504.02246#S3.F2)demonstratesC⋆\\star’s workflow using the verification of theclearfunction shown in[section2](https://arxiv.org/html/2504.02246#S2)\. Note that here we reinterpret the commented\-out proof\-code blocks in lines 9, 21, and 23 ofas they are*not*inserted into the implementation code\.[Fig\.2\(a\)](https://arxiv.org/html/2504.02246#S3.F2.sf1)is the assembled operational proof program: lines 1–15 are three code segments split by proof\-code blocks in lines 7 and 18 of\. In the main function, we use the built\-in functionfeed\_program\_segmentto feed a code segment to the symbolic\-execution engine, as we will explain below about the second stage\.

1code\_segment\_tseg1=

2voidclear\(void\*to,intlen\)

3\[\[require\(\.\.\.\)\]\]

4\[\[ensure\(\.\.\.\)\]\]

5\{\*/;

6code\_segment\_tseg2=

7inti=0;

8while\(i<len\)

9\[\[invariant\(\.\.\.\)\]\]

10\{\*/;

11code\_segment\_tseg3=

12\*\(\(char\*\)to\+i\)=\(char\)0;

13i=i\+1;

14\}

15\}\*/;

16intmain\(void\)\{

17feed\_program\_segment\(seg1\);

18termparams=\.\.\.;

19feed\_program\_segment\(seg2\);

20single\_out\_location\(\);

21feed\_program\_segment\(seg3\);

22\}

\(a\)Operational Proof Program
1termvc1=

2\(line9of\)\*/;

3termvc2=

4\(line21of\)\*/;

5termvc3=

6\(line23of\)\*/;

7

8thmproof1\(\)\{

9

10\}

11thmproof2\(\)\{

12

13\}

14thmproof3\(\)\{

15

16\}

17

18intmain\(void\)\{

19assert\_prove\(proof1\(\),vc1\);

20assert\_prove\(proof2\(\),vc2\);

21assert\_prove\(proof3\(\),vc3\);

22\}

\(b\)Residual Proof Program

Figure 2\.Demonstration ofC⋆\\star’s workflow using the running example in[section2](https://arxiv.org/html/2504.02246#S2)\.
#### Operational proof checking stage\.

In the second stage, theC⋆\\starworkflow executes the operational proof program obtained from the translation stage\. As discussed in[section2](https://arxiv.org/html/2504.02246#S2),C⋆\\starsupports two styles of program verification, namely declarative and operational:

- •In the declarative style, the user asserts expected symbolic states at specific program points\. The symbolic\-execution engine uses the asserted symbolic state for further execution and produce*verification conditions*as output\. These verification conditions are gathered and will be proved*in batch*later in the*residual proof checking stage*\.
- •In the operational style, the user directly manipulates the symbolic state through proof\-code blocks, which are executed interactively with the symbolic execution\. In this way, the operational proof checking phase is naturally*real\-time*: the proof\-code blocks are executed*interleaved*with symbolic execution, feeding the annotated program segments incrementally to the symbolic\-execution engine\.

More specifically, theC⋆\\starworkflow handles the execution of each proof block as follows\. First, the last annotated program segment—as some serializable data—is fed to the symbolic\-execution engine\. Next, the proof\-code block, which is normal C code, is executed in the proof\-supporting runtime \(see Remark[3\.2](https://arxiv.org/html/2504.02246#S3.Thmtheorem2)below\)\. Finally, the current symbolic state is updated according to the execution results of the proof\-code block: recall that a proof\-code block should fetch the symbolic state by callingget\_symbolic\_state, do transformations on it with proofs, and then callset\_symbolic\_stateat the end to update the symbolic state in the symbolic\-execution engine\. The proof program shown in[Fig\.2\(a\)](https://arxiv.org/html/2504.02246#S3.F2.sf1)implicitly calls these functions in the code ofsingle\_out\_location, i\.e\.,\.

#### Residual proof checking stage\.

In the third stage, theC⋆\\starcompiler collects the output of the symbolic\-execution engine and creates the*residual proof program*, which is aC⋆\\starprogram purely consisting of global proof\-code blocks\. This program contains proof goals for every undischarged verification condition generated during symbolic execution, which are to be addressed in theC⋆\\starproof environment, either by the programmers or with assistance from proof experts\. Those verification conditions arise from the declarative style of verification: recall that at each assertion or invariant, it is obliged forC⋆\\starusers to prove the entailment from the maintained symbolic state \(by the symbolic\-execution engine\) to the asserted state\.[Fig\.2\(b\)](https://arxiv.org/html/2504.02246#S3.F2.sf2)shows the residual proof program for the running example in[section2](https://arxiv.org/html/2504.02246#S2): lines 1–6 are three verification conditions generated by the symbolic\-execution engine, lines 8–16 are user\-provided proof code for the three verification conditions, respectively, and the main function executes the proof code the check if they indeed prove the verification conditions\.

### 3\.2\.Interface forC⋆\\starUsers

Figure 3\.A summary of the verification\-specific interface thatC⋆\\starprovides to users\.As overviewed in[section2](https://arxiv.org/html/2504.02246#S2),C⋆\\starextends the C programming language with two categories of verification\-specific syntactic constructs: \(i\) specifications and intermediate assertions, and \(ii\) proof\-code blocks\.[Fig\.3](https://arxiv.org/html/2504.02246#S3.F3)summarizes these constructs, providing an accessible interface forC⋆\\starusers\. In this section, we explain our design of this interface and at the end exemplifyC⋆\\star’s extensibility in proof support using the implementation oflocal\_applyfromC⋆\\star’s standard proof\-support library\.

#### Verification\-specific attributes

C⋆\\starintroduces attributes\[\[require\]\],\[\[ensure\]\],\[\[parameter\]\], and\[\[argument\]\]concerning function specifications,\[\[assert\]\]and\[\[invariant\]\]for intermediate assertions within implementation code, as well as\[\[proof\]\]for embedding proof\-code blocks\.

The attributes\[\[require\]\]and\[\[ensure\]\]specify a function’s*pre\-condition*and*post\-condition*, respectively, both containing C expressions that evaluate to atermvalue of object\-logic typehprop, i\.e\., a separation\-logic predicate\. Both the pre\- and post\-condition can reference function parameters, and the post\-condition can additionally reference the function’s returned value using the preserved symbol\_\_result\. The attribute\[\[parameter\(‘var:type‘\)\]\]introduces a*ghost*parametervarof object\-logic typetypethat denotes a universally quantified logical variable for the function specification\. Correspondingly, the\[\[argument\(‘var=value‘\)\]\]—used before a function call—instantiates the ghost variable with an object\-logic term\.[Fig\.3](https://arxiv.org/html/2504.02246#S3.F3)illustrates the usage of parameter and argument attributes using a C functionreversethat reverses a linked list in\-place: the parameterlis a logic\-level integer list that encodes the content of the linked list pointed to byp, where the \(user\-defined\) separation\-logic predicatell\_repr\(p,l\)expresses such encoding\.

Similar to\[\[require\]\]and\[\[ensure\]\], the\[\[assert\]\]and\[\[invariant\]\]attributes take a C expression as input, which evaluates to a separation\-logic predicate\. The\[\[assert\]\]attribute inserts a static assertion about the symbolic state at a program point, supporting a*declarative*verification style: if non\-trivial reasoning is required to prove that the maintained symbolic state entails the asserted state, a verification condition is generated by the symbolic\-execution engine\. We will explain this workflow in detail in[section3\.1](https://arxiv.org/html/2504.02246#S3.SS1)\. After processing an assertion, the symbolic\-execution engine will update the symbolic state accordingly\. The\[\[invariant\]\]attribute also inserts an assertion but it asserts a symbolic state expected at the start of each loop iteration, hence its name*invariant*\. Currently, onlywhileloops are supported, and usingbreakorcontinuewill lead the symbolic\-execution engine to generate additional verification conditions for the additional control\-flow paths\.

The\[\[proof\]\]attribute wraps a proof\-code block\. Proof\-code blocks may contain arbitrary C code, having access to the LCF\-style proof kernel and the symbolic\-execution engine\. There are two kinds of proof\-code blocks: \(i\)*local proof blocks*, used within implementation code \(e\.g\., inside a function body\), primarily for*operational*verification and symbolic\-state transformation, and \(ii\)*global proof blocks*, used outside any implementation code, typically for defining common proof functions or theorems\. Typically, all code in a proof\-support library \(e\.g\.,cstarlib\.h\) is within global proof blocks\. Within a local proof block, the user can reference bindings declared in prior proof blocks in the same function body, as well as bindings declared in global proof blocks\.

#### Specifications and intermediate assertions

Inside the verification\-specific attributes,C⋆\\starprovides a*quotation*syntax \(delimited by‘\.\.\.‘\)\. It allows the user to construct object\-logic terms using concrete syntax representations and avoid the verbosity of calling term constructors explicitly\. Inside quotations, the user can use the*anti\-quotation*mechanism \(escaped using$\{var:type\}\) for splicing in computed sub\-terms stored in program variables\. Together, these two syntax extensions offer a simple yet expressive way to build object\-logic terms\.[Fig\.3](https://arxiv.org/html/2504.02246#S3.F3)summarizes the concrete syntax for separation\-logic predicates and other frequently used object\-logic terms and types\. There are a few unsual notational conventions, which arise from the LCF\-style proof kernel employed byC⋆\\star\. In the object logic, integer literals \(i\.e\., terms of object\-logic typeinteger\) take the form&n, wherenis a natural number\. The logic\-level representation of an address is an integer value, e\.g\.,&"x"denotes the address of the program variable namedx\. We reuse C’s&&and\|\|operators to encode logic\-level conjunction an disjunction, respectively, and use==\>for standard logical implication\. Separation\-logic entailments are treated as propositions \(i\.e\., terms of object\-logic typebool\): the binary operator\|\-\-takes two separation\-logic predicateshp1andhp2and produces a propositionhp1\|\-\-hp2, whose meaning is that if a heap satisfieshp1, then it also satisfieshp2\.

InC⋆\\star, separation\-logic predicates in specifications and intermediate assertions must adhere to a specific form to enable automated symbolic execution\. This specific form is known as the*symbolic heaps*\([Berdine et al\., 2005](https://arxiv.org/html/2504.02246#bib.bib5)\), and has the following structure:

\(SymHeap\)∃x1,…,xk\.\(P1∧⋯∧Pm\)∧\(Q1∗⋯∗Qn\),\\exists x\_\{1\},\\ldots,x\_\{k\}\.\\ \(P\_\{1\}\\land\\cdots\\land P\_\{m\}\)\\land\(Q\_\{1\}\*\\cdots\*Q\_\{n\}\)\\ ,wherexix\_\{i\}’s are existentially quantified logical variables,∧\\landdenotes non\-separating conjunction, i\.e\., standard logical conjunction, and∗\*represents separating conjunction\. ThePiP\_\{i\}’s are*pure facts*—expressions in the form ofpure\(p\)that state properties about the global heap\. TheQjQ\_\{j\}’s, known as*spatial facts*, consist of either primitive maps\-to predicates \(i\.e\.,data\_atorundef\_data\_at\) which are visible to the symbolic\-execution engine, or user\-defined predicates \(e\.g\.,array\_at\) whose internal structure can be arbitrary and are opaque to the symbolic\-execution engine\. These spatial facts represent separately\-owned local fragments of the heap\. We often use the derived formfact\(p\)=pure\(p\)&&empto describe pure properties\. The derived form satisfies thatpure\(p\)&&H=fact\(p\)\*H\. This formulation allows symbolic heaps to be uniformly represented as separating conjunctions of pure and spatial facts, avoiding the need for non\-separating conjunction\.

Before symbolically executing any primary program statement, the symbolic\-execution engine verifies that the current symbolic state includes the necessary primitive maps\-to predicates for all accessed memory locations\. Once this requirement is satisfied, the engine updates the symbolic state as needed, preserving the symbolic form, and possibly generates side conditions to guarantee safe execution, i\.e\., no runtime error or undefined behavior\.

In addition to the primitive predicates and predicates provided in the standard library,C⋆\\starusers can derive and use their customized predicates\. For instance, thehiterfunction in the standard proof\-support library, defined in object\-logic ashiterhps=fold\_right\(\*\*\)hpsempusing the higher\-order functionfold\_right, takes a list of separation\-logic predicateshpsand returns their*iterated separating conjunction*\. We will explain how to implement derived predicates later in this section\.

#### Proof\-code interface with symbolic execution

InC⋆\\star, a local proof\-code block for performing operational verification retrieves the current symbolic state from the symbolic\-execution engine by calling a built\-in functionget\_symbolic\_state\(\)\. For example, the initial symbolic state can be obtained withtermpre\_state=get\_symbolic\_state\(\)\. At the end of the proof\-code block, the symbolic state can be updated using a call toset\_symbolic\_state\(th\), wherethis a theorem proving the separation\-logic entailment from the current symbolic state \(pre\_state\) to a new state \(new\_state\)\. This updated statenew\_stateis then set as the current symbolic state\. Recallin[section2](https://arxiv.org/html/2504.02246#S2)for an example of using the interface to do local transformations on the symbolic state\.

#### Proof\-code interface with LCF\-style proof kernel

In an LCF\-style proof environment like that inC⋆\\star, two fundamental types are provided for logical reasoning:term, representing terms in the object logic, andthm, denoting proven theorems\. These types are treated as abstract types inC⋆\\star, ensuring that users can only manipulate them through the library functions provided by the LCF proof kernel, forbidding direct access to internal data structures\.

As summarized in[Fig\.3](https://arxiv.org/html/2504.02246#S3.F3), to work withtermvalues, the proof kernel offers a set of functions acting as constructors, destructors, discriminators, and equality checkers, among other utilities\. Forthmvalues, the kernel provides the primitive rules needed to prove theorems\. These rules encompass both separation\-logic entailment rules and higher\-order logic rules for general reasoning\. Additionally, functions for checking if a proof goal is achieved and for accessing the hypotheses and conclusion of a theorem are available\.

The programmability ofC⋆\\star’s LCF\-style proof kernel allows users to extend its functionality by defining customized derived rules or proof\-search routines as C functions on top of the primitive proof rules\. Furthermore, besides the built\-in types such asctypeandhprop, as well as standard functions likesizeof, the kernel’s*definitional mechanism*enables users to define new \(inductive\) types, e\.g\.,int\_listin[Fig\.3](https://arxiv.org/html/2504.02246#S3.F3), as well as \(recursive\) functions, e\.g\.,nthin[Fig\.3](https://arxiv.org/html/2504.02246#S3.F3)\. Such definitional mechanism is also used to define new sepeartion\-logic predicates, such ashitermentioned earlier in this section\. This flexibility makesC⋆\\starexpressive for a wide range of verification needs\.

#### Extensible and programmable proof support

With the programmability of LCF\-style proof support, proof experts can develop custom proof libraries to simplify common proof patterns, offering high\-level derived proof rules and collections of frequently used mathematical properties\.

For example, a typical task in operational\-style verification is justifying local transformations performed on the symbolic state\. By*local transformations*, we mean picking out specific conjuncts from a symbolic heap, applying a proved\-correct separation\-logic entailment to these conjuncts, and leaving the rest of the symbolic heap unchanged\. Separation logic inherently supports such local transformations; however, using only primitive rules of separation logic—some of which are listed in[Fig\.4](https://arxiv.org/html/2504.02246#S3.F4)— requires manually lifting affected conjuncts through layers of separating conjunctions and specifying frames for each transformation\. This can be tedious and lead to proof code cluttered with structural manipulations, which detract from the intuitive reasoning process\.

H1∗H2⊢⊢H2∗H1​hsep\-comm​\(H1∗H2\)∗H3⊢⊢H1∗\(H2∗H3\)​hsep\-assoc​H1⊢H1′H1∗H2⊢H1′∗H2​hsep\-cancel\-right​∀x\.\(H⊢H′\)\(∃x\.H\)⊢\(∃x\.H′\)​hexists\-monotone\\frac\{\\ \}\{H\_\{1\}\*H\_\{2\}\\reflectbox\{$\\vdash$\}\\mkern\-5\.0mu\\vdash H\_\{2\}\*H\_\{1\}\}\\hskip 9\.24994pt\\textsc\{hsep\-comm\}\\frac\{\\ \}\{\(H\_\{1\}\*H\_\{2\}\)\*H\_\{3\}\\reflectbox\{$\\vdash$\}\\mkern\-5\.0mu\\vdash H\_\{1\}\*\(H\_\{2\}\*H\_\{3\}\)\}\\hskip 9\.24994pt\\textsc\{hsep\-assoc\}\\frac\{H\_\{1\}\\vdash H\_\{1\}^\{\\prime\}\}\{H\_\{1\}\*H\_\{2\}\\vdash H\_\{1\}^\{\\prime\}\*H\_\{2\}\}\\hskip 9\.24994pt\\textsc\{hsep\-cancel\-right\}\\frac\{\\forall x\.\\ \(H\\vdash H^\{\\prime\}\)\}\{\(\\exists x\.\\ H\)\\vdash\(\\exists x\.\\ H^\{\\prime\}\)\}\\hskip 9\.24994pt\\textsc\{hexists\-monotone\}Figure 4\.Selected separation\-logic rules for structural manipulations\.To alleviate the need for manually performing such structural manipulations, we implemented a derived rule calledlocal\_applyin our standard proof\-support librarycstarlib\.h\. Considers the simple case where only one conjunct is affected by the transformation, the automation process oflocal\_applycan be described in four steps as follows\.

1. \(1\)Repeatedly destruct existential binders in the symbolic heap of the form \([SymHeap](https://arxiv.org/html/2504.02246#S3.Ex1)\)\.
2. \(2\)Find the affected conjunct and lift it to the far\-left side of the symbolic heap by using thehsep\-commandhsep\-assocrules repeatedly\.
3. \(3\)Apply thehsep\-cancel\-rightrule with other conjuncts to the right as the frame\.
4. \(4\)Repeatedly add back existential binders using thehexists\-monotonerule\.

As a concrete code example, we present the proof functionsep\_lift\_onefor performing the second step in\. It assumes the input symbolic heapseptermis a right\-associated separating conjunction\. It first calls the derived rulehsep\_move, getting a generalized equality theoremlift\_to\_left\(line 4\) for moving the target conjunct out to the left for one layer when it is in the left position of the inner symbolic heap, in one step\. It then tries to find the target conjunct recursively:

1. \(1\)If the target conjunct is never found, it returnsNULL\.
2. \(2\)If the target conjunct is at the far\-right position, it rewrites it using thehsep\-commrule\.
3. \(3\)Otherwise, it uses the equality theoremlift\_to\_leftto move the target conjunct out to the left for one layer\. The lifting steps work in bottom\-up way during unwinding the recursive calls\.

1thmsep\_lift\_one\(termtarget,termsepterm\)

2

3\{

4thmlift\_to\_left=hsep\_move\(target\);

5

6hp1\*\*$\{target:hprop\}\*\*hp2\-\|\-$\{target:hprop\}\*\*hp1\*\*hp2\*/

7

8if\(is\_sep\(septerm\)\)\{

9terml=left\_of\_sep\(septerm\),r=right\_of\_sep\(septerm\);

10if\(equals\_term\(target,l\)\)\{returnrewrite\(lift\_to\_left,septerm\);\}

11else\{

12if\(is\_sep\(r\)\)\{

13thmstep1=rewrite\(sep\_lift\_one\(target,r\),septerm\);

14thmstep2=rewrite\(lift\_to\_left,consequent\(conclusion\(step1\)\)\);

15returntrans\(step1,step2\);

16\}elseif\(equals\_term\(target,r\)\)

17returnrewrite\(symm\(hsep\_comm\(target\)\),septerm\);

18\}

19\}elseif\(equals\_term\(target,septerm\)\)\{returnrefl\(septerm\);\}

20returnNULL;

21\}

Listing 3:C⋆\\starcode ofsep\_lift\_one\.

## 4\.Implementation and Evaluation

In this section, we describe our prototype implementation ofC⋆\\starand our evaluation of it\. In[section4\.1](https://arxiv.org/html/2504.02246#S4.SS1), we discuss some aspects of our prototypeC⋆\\starimplementation diverged from the core design in[section3](https://arxiv.org/html/2504.02246#S3)\. In[section4\.2](https://arxiv.org/html/2504.02246#S4.SS2), we present an empirical evaluation of our prototype implementation on a suite of C benchmark programs and report some interesting findings on usingC⋆\\starfor program verification\.

### 4\.1\.Implementation Notes

Following the workflow described in[section3\.1](https://arxiv.org/html/2504.02246#S3.SS1), our implementation consists of three main components: theC⋆\\starcompiler, the LCF\-style proof kernel, and the symbolic\-execution engine\.

#### Implementing theC⋆\\starcompiler

TheC⋆\\starcompiler, implemented in OCaml, processes C code withC⋆\\star\-specific attributes, managing syntax extensions \(quotation and anti\-quotation\) and translating them to invocations of term\-parsing functions and substitution primitives\. The compiler also assembles code in the proof blocks to form a proof program that executes in the proof\-supporting runtime\. Note that the proof program is a C program\. Specifically, global proof blocks are moved to the beginning of the generated C program, and each function in the implementation code creates a proof function, with local proof blocks appended in the order of their appearance\. It also aligns the concrete annotation syntax \(and separation\-logic assertion syntax\) used inC⋆\\starwith the external symbolic execution\-engine\.

#### Reusing HOL Light proof kernel

In the implementation ofC⋆\\star, we reuse the LCF\-style proof kernel of the HOL Light prover\([Harrison, 2009](https://arxiv.org/html/2504.02246#bib.bib18)\), a minimal implementation of higher\-order logic in OCaml\. This avoids the need to build a new LCF\-style kernel from scratch in C, while leveraging the extensive libraries available in HOL Light for mathematical reasoning\. To support separation\-logic entailment proofs needed in program verification, we axiomatize a separation logic theory in HOL Light with a concrete memory model in mind, interpreting the heap as a finite mapping from addresses to bytes and treating integers and pointers the same in higher\-order logic\.

#### Interfacing with the symbolic execution engine

In the ideal workflow illustrated in[Fig\.1](https://arxiv.org/html/2504.02246#S3.F1), proof programs communicate with the symbolic\-execution engine via functions likeget\_symbolic\_state\(\),set\_symbolic\_state\(th\), andfeed\_program\_segment\(prog\)\. However, we currently lack access to the internal states of the external symbolic\-execution engine, making it challenging to implement this interactive workflow directly\. Consequently, we currently rely on the annotations that the symbolic\-execution engine supports for communication\. To simulate the interleaving execution pattern in the ideal workflow, we need to run the symbolic\-execution engine twice for each proof block: once for getting the symbolic state and once for setting it after running the proof code\. This is done manually for now\.

### 4\.2\.Empirical Evaluation

To evaluate the effectiveness of our prototype implementation ofC⋆\\star, we selected a suite of small C programs as benchmarks and verified their functional correctness usingC⋆\\star\. Most examples are adapted from the VeriFast repository\([Jacobs et al\., 2011](https://arxiv.org/html/2504.02246#bib.bib21)\), while the buddy allocator example is drawn from CN\([Pulte et al\., 2023](https://arxiv.org/html/2504.02246#bib.bib36)\)\. Some additional examples were crafted manually to testC⋆\\star’s handling of complex control\-flow structures\. This benchmark allows us to \(i\) test the functionality of theC⋆\\startoolchain, including its frontend parser, proof\-supporting runtime, and the translation phase, \(ii\) assess the expressiveness ofC⋆\\star’s reasoning capabilities, and \(iii\) evaluate the usability ofC⋆\\star’s hybrid operational and declarative proof approach\.

Table 2\.Evaluation ofC⋆\\star\. “Impl” is short for “Implementation Code\.” “PB” is short for “Proof Block\.” “VC” is short for “Verification Condition\.” “Spec” is short for “Specficiation\.” “Assert” is short for “Assertion\.”A complete list of the benchmark is shown in[Tab\.2](https://arxiv.org/html/2504.02246#S4.T2)and the source code of all benchmark programs is included in the Supplementary Material\. We chose these programs to encompass a broad spectrum of reasoning patterns, including shared memory access \(\#1\), control\-flow constructs \(\#2\), dynamic memory management and interaction with external functions \(\#3\), complex model\-level reasoning \(\#4\), and a real\-world case study \(\#5\)\.[Tab\.2](https://arxiv.org/html/2504.02246#S4.T2)presents statistics regarding the code size of each benchmark program\. The column “\#Line of Impl” lists the number of lines of implementation code\. The total number of lines in each benchmark program is significantly larger due to the inclusion of proof code, whose statistics is given in the column “\#Line of Proof,” as well as specifications and assertions, whose statistics is given in the column “\#Line of Spec/Assertion\.” We also include \(i\) the number of proof blocks for the operational style of verification and \(ii\) the number of verification conditions for the declarative style of verification\.

#### Coverage of C language features

The evaluation demonstratesC⋆\\star’s support for core C features, especially those that create flexible aliasing patterns and complex control flow structures:

- •Control\-flow constructs, including multiple branching \(if\.\.\.elseif\.\.\.\), \(mutually\) recursive functions,breakandcontinue, and \(early\)return\. Benchmark programsaddress\_of\_local,multi\_branch,mutually\_recursive, andno\_returnuse some of these constructs\.
- •Shared memory access, covering global variables, arrays, addressable local variables, and \(multi\-level\) pointer indirections\. Benchmark programsaddress\_of\_local,globals, andswapmake use of shared memory access\.
- •Dynamic memory management and interaction with \(formally specified\) external functions, tested viamallocandfree\. The benchmark programmalloc\_freedemonstrate those features\.

Currently, our prototype implementation does not supportswitchstatement,goto, or other looping constructs \(i\.e\.,foranddowhile\)\. We leave supporting those features for future work\.

#### Complex logical reasoning

The benchmarks also illustrateC⋆\\star’s capability for performing complex logic\-level reasoning\. The expressiveness of higher\-order logic used inC⋆\\starenables users to define functional models \(as inductive data types, e\.g\., lists or trees\) and also \(well\-founded\) recursive functions that operate on these models \(e\.g\., reversing a list\), using high\-level definitional mechanisms\. Users can also define recursive representation predicates to link the entry points of concrete memory structures to their functional models, a technique typical of separation\-logic\-based program reasoning\([Charguéraud, 2016](https://arxiv.org/html/2504.02246#bib.bib7)\)\. In several instances within our benchmark, we leveraged the pre\-existing proof libraries of HOL Light, thereby reducing the effort required for model\-level reasoning\. Nonetheless, for the benchmark programreverse, we proved four logic\-level reasoning lemmas and two ownership\-related reasoning lemmas, which are reusable for reasoning about linked lists\.

The proof code in those benchmark programs extensively usesC⋆\\star’s standard proof\-support library\. In addition tolocal\_applydescribed in[section3\.2](https://arxiv.org/html/2504.02246#S3.SS2), our proof\-support library includes other reusable derived rules\. For example,sep\_normalize\(t\)transforms a heap proposition into a canonical form,sep\_lift\(l,t\)lifts a sub\-part of the heap propositiontto the far\-left side, generalizing thesep\_lift\_onefunction in, andsep\_reorder\(t1,t2\)verifies if two heap propositions are reorderings of each other \(moduloα\\alpha\-renaming of bound variables\)\.

#### A real\-world case study: buddy allocator

Inspired by CN\([Pulte et al\., 2023](https://arxiv.org/html/2504.02246#bib.bib36)\), we appliedC⋆\\starto a more challenging real\-world case study: the attach function of the buddy allocator used in pKVM\([Project, 2024](https://arxiv.org/html/2504.02246#bib.bib33)\)\. A buddy allocator manages memory in blocks of size2o×42^\{o\}\\times 4KB, whereo∈0,1,…,𝑚𝑎𝑥​\_​𝑜𝑟𝑑𝑒𝑟−1o\\in\{0,1,\\ldots,\\mathit\{max\\\_order\}\-1\}denotes the order of the block\. Each block is aligned according to its size, maintaining an invariant about the alignment for all blocks\.

Two blocks are called*buddies*if they \(i\) are adjacent, \(ii\) have the same order, and \(iii\) can be merged into a larger block of the next order while preserving alignment\. Allocatable memory is divided into pools, each representing a contiguous range of pages\. Every pool maintains a doubly\-linked list of free blocks for each order, and the allocator searches these lists for a free block of the required size during memory allocation\. Readers may refer to\([Pulte et al\., 2023](https://arxiv.org/html/2504.02246#bib.bib36)\)for further details on the data structures and helper functions used in this case study\.

We verified theattach\_pagefunction, shown in[Fig\.5\(a\)](https://arxiv.org/html/2504.02246#S4.F5.sf1), from the implementation of the buddy allocator\. This function operates by receiving a released block, identifying any adjacent free buddy block in the pool, and merging them to form a larger free block\. This merging process continues iteratively until no more free buddies are found or the maximum order is reached\. The resulting block is then added back to the pool\. The loop invariant of the while loop in the implementation code is shown in[Fig\.5\(b\)](https://arxiv.org/html/2504.02246#S4.F5.sf2)\. An interesting finding during verification was that the specifications in CN\([Pulte et al\., 2023](https://arxiv.org/html/2504.02246#bib.bib36)\)were not sufficient to guarantee that all free blocks are present in a doubly\-linked list\. Despite this, we adhered to these weaker specifications for simplicity in our verification efforts\.

structhyp\_page\*\_\_hyp\_vmemmap;

staticvoidattach\_page\(

structhyp\_pool\*pool,structhyp\_page\*pg

\)\{

structhyp\_page\*buddy=NULL;

u8order=pg\-\>order;

pg\-\>order=\(u8\)HYP\_NO\_ORDER;

u8max\_order\_=pool\-\>max\_order;

memset\_page\_zero\(pg,order\);

buddy=\_\_find\_buddy\_avail\(pool,pg,order\);

while\(\(order\+1\)<max\_order\_&&

buddy\!=NULL\)\{

page\_remove\_from\_list\_pool\(pool,buddy\);

buddy\-\>order=\(u8\)HYP\_NO\_ORDER;

pg=min\(pg,buddy\);

order=order\+1;

buddy=\_\_find\_buddy\_avail\(pool,pg,order\);

\}

pg\-\>order=order;

page\_add\_to\_list\_pool\(pool,pg,order\);

\}

\(a\)The implementation code\.
\[\[invariant\(‘

existsbuddy\_vbiinv\_linv\_dlinv\_hliorder\_vpg\_v\.

data\_at\(&"max\_order",Tuchar,&max\_order\)\*\*

data\_at\(&"order",Tuchar,&order\_v\)\*\*

data\_at\(&"pg",Tptr,pg\_v\)\*\*

data\_at\(&"buddy",Tptr,buddy\_v\)\*\*

data\_at\(&"pool",Tptr,pool\_pre\)\*\*

data\_at\(&"\_\_hyp\_vmemmap",Tptr,vmemmap\)\*\*

\(dlist\_head\_reprpool\_pre0max\_orderinv\_hl\)\*\*

\(free\_area\_repr

\(is\_free\_1stinv\_l\)startendinv\_l\)\*\*

\(free\_area\_head\_repr

\(is\_free\_1stinv\_l\)startendinv\_dl\)\*\*

\(store\_pageinfo\_arrayvmemmapstartendinv\_l\)\*\*

\(store\_zero\_array

\(i2vaddri\)0\(PAGE\_SIZE\*\(2EXPorder\_v\)\)

\(PAGE\_SIZE\*\(2EXPorder\_v\)\)\)\*\*

$\{other\_facts\_and\_representation\_predicates:hprop\}

‘\)\]\]

\(b\)The invariant of the loop\.

Figure 5\.Theattach\_pagefunction\.
#### Experience report

The experience of two undergraduate students in usingC⋆\\starfor benchmark evaluation reveals several usability issues of the current prototype implementation:

- •*IDE support\.*The lack of an IDE that shows symbolic states alongside code was a major pain point\. Currently, users must run the symbolic execution engine manually and inspect symbolic states from its lengthy output, which interrupts the workflow\. Developing an IDE forC⋆\\star, e\.g\., as an editor plugin, is left for future work\.
- •*Proof automation\.*C⋆\\starlacks automation for discharging trivial facts, making simple proofs time\-consuming\. This is partly due to the absence of solver\-aided proof automation, heavily relied on by tools like CN\([Pulte et al\., 2023](https://arxiv.org/html/2504.02246#bib.bib36)\)and VeriFast\([Jacobs et al\., 2011](https://arxiv.org/html/2504.02246#bib.bib21)\)\. Looking forward, we plan to provideC⋆\\staran interface to encode and delegate proof obligations to external automated theorem provers or frameworks such as Z3\([de Moura and Bjørner, 2008](https://arxiv.org/html/2504.02246#bib.bib11)\)and Why3\([Filliâtre and Paskevich, 2013](https://arxiv.org/html/2504.02246#bib.bib12)\)\.
- •*Proof\-support library\.*Writing separation\-logic entailment proofs inC⋆\\starcurrently requires considerable boilerplate code, leading to long and repetitive proof code\. This issue arises becauseC⋆\\starlacks a rich set of derived rules for handling separation\-logic reasoning, unlike mature frameworks such as Iris\([Krebbers et al\., 2017](https://arxiv.org/html/2504.02246#bib.bib24)\), VST\([Cao et al\., 2018](https://arxiv.org/html/2504.02246#bib.bib6)\), or CFML\([Charguéraud, 2020](https://arxiv.org/html/2504.02246#bib.bib8)\)\. In our future work, we expect that expandingC⋆\\star’s proof support libraries with more derived rules could improve the conciseness of proof code and developer productivity\.

## 5\.Related Work

#### Live Verification framework

The Live Verification framework\([Gruetter et al\., 2024](https://arxiv.org/html/2504.02246#bib.bib16)\)is a recently proposed framework with a similar goal of enabling its users to verify their low\-level code as they write it\. The framework is embedded in the Coq proof assistant and provides real\-time display of the symbolic state at the cursor position in the goal panel\. After a function has been given a prototype with formal specifications, users develop the function body incrementally by either writing the next line of implementation code, or writing Ltac proof scripts to shift the view on the symbolic state or discharge generated side conditions\. When this derivation process is finished, a correctness proof is produced alongside the assembled implementation code\. With some clever tricks, these Ltac source files can also be viewed as ordinary C code \(with Ltac proof scripts in comments\) and compiled directly with C compilers\.

A key difference betweenC⋆\\starand the Live Verification framework isC⋆\\star’s focus on accessibility for conventional programmers\. In the Live Verification framework, proof development and customization of proof automation require proficiency in Coq’s Ltac tactic language, which diverges from the imperative programming experience familiar to programmers\. In contrast,C⋆\\starallows proof code to be written directly in the same language as the implementation code, making it more approachable for conventional programmers\.

#### VeriFast

VeriFast\([Jacobs et al\., 2011](https://arxiv.org/html/2504.02246#bib.bib21)\)is a state\-of\-the\-art symbolic execution and separation logic\-based automated verification tool for C and Java\. It has a custom specification language that allows users to define inductive data types, structurally recursive functions, and recursive representation predicates\. VeriFast emphasizes predictable automation: during symbolic execution, users manually unfold and fold predicates using the proof commandsopenandclose\. A restricted form of existential quantification is supported in the form of pattern matching, and reasoning on first\-order values are delegated to the SMT solver\. When inductive reasoning is required, it supports user\-written ghost lemma functions, which are verified like the implementation code but require proof of termination and must be observationally pure\. VeriFast can handle a substantial subset of C features\.

The primary distinction betweenC⋆\\starand VeriFast lies in the extensibility of their proof support\. In VeriFast, proof support is limited to a fixed set of built\-in ghost statements and basic induction capabilities using lemma functions\. On the other hand,C⋆\\starenables users to develop custom proof rules and automation functions, offering greater flexibility and expressiveness for complex verification tasks\. Also, this extensibility allows experts to create high\-level reasoning abstractions that are accessible to programmers\.

#### CN

CN\([Pulte et al\., 2023](https://arxiv.org/html/2504.02246#bib.bib36)\)is an ownership and refinement type system for C, targeting the verification of real\-world systems software\. CN aims for predictable proof automation, employing the Liquid types\([Rondon et al\., 2008](https://arxiv.org/html/2504.02246#bib.bib39)\)approach for decidable automation using an SMT backend, with heuristics for instantiating quantifiers\. It supports sound ownership reasoning at the type level using idea similar to capabilities\([Ahmed et al\., 2007](https://arxiv.org/html/2504.02246#bib.bib2)\), split the type of a heap fragment into a linear capability type and an unrestricted pointer type for flexible aliasing commonly found in real\-world code\. Additionally, CN is grounded on a realistic semantics, Cerberus\([Memarian et al\., 2016](https://arxiv.org/html/2504.02246#bib.bib30)\), which accurately models a large fragment of ISO C\.

## 6\.Conclusion

In this paper, we presentedC⋆\\star, a new system and language design for verified programming in C\.C⋆\\starprovides three key features: \(i\) language\-level integration supporting both declarative and operational styles of verification, \(ii\) comprehensive reasoning capabilities within an expressive logic using C’s programming paradigm, and \(iii\) support for real\-time verification\. It builds upon the established techniques of separation logic\-based symbolic execution for modular program reasoning, as well as the LCF\-style approach to programming proofs\. We implemented a prototype ofC⋆\\starand evaluated its effectiveness by developing verified C programs using a suite of benchmark programs\. In the future, we plan to develop an IDE forC⋆\\starto enable interactive program verification, interfaceC⋆\\starwith solved\-aided proof automation to reduce proof efforts, and develop more proof\-support libraries forC⋆\\star\.

## References

- Ahmed et al\.\(2007\)Amal Ahmed, Matthew Fluet, and Greg Morrisett\. 2007\.L3\{\}^\{\\mbox\{3\}\}: A Linear Language with Locations\.*Fundam\. Informaticae*77, 4 \(2007\), 397–449\.[http://content\.iospress\.com/articles/fundamenta\-informaticae/fi77\-4\-06](http://content.iospress.com/articles/fundamenta-informaticae/fi77-4-06)
- Amani et al\.\(2016\)Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O’Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby C\. Murray, Gerwin Klein, and Gernot Heiser\. 2016\.CoGENT: Verifying High\-Assurance File System Implementations\. In*Proceedings of the Twenty\-First International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2016, Atlanta, GA, USA, April 2\-6, 2016*, Tom Conte and Yuanyuan Zhou \(Eds\.\)\. ACM, 175–188\.[https://doi\.org/10\.1145/2872362\.2872404](https://doi.org/10.1145/2872362.2872404)
- Appel \(2011\)Andrew W\. Appel\. 2011\.Verified Software Toolchain \- \(Invited Talk\)\. In*Programming Languages and Systems \- 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26\-April 3, 2011\. Proceedings**\(Lecture Notes in Computer Science, Vol\. 6602\)*, Gilles Barthe \(Ed\.\)\. Springer, 1–17\.[https://doi\.org/10\.1007/978\-3\-642\-19718\-5\_1](https://doi.org/10.1007/978-3-642-19718-5_1)
- Berdine et al\.\(2005\)Josh Berdine, Cristiano Calcagno, and Peter W\. O’Hearn\. 2005\.Symbolic Execution with Separation Logic\. In*Programming Languages and Systems, Third Asian Symposium, APLAS 2005, Tsukuba, Japan, November 2\-5, 2005, Proceedings**\(Lecture Notes in Computer Science, Vol\. 3780\)*, Kwangkeun Yi \(Ed\.\)\. Springer, 52–68\.[https://doi\.org/10\.1007/11575467\_5](https://doi.org/10.1007/11575467_5)
- Cao et al\.\(2018\)Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, and Andrew W\. Appel\. 2018\.VST\-Floyd: A Separation Logic Tool to Verify Correctness of C Programs\.*J\. Autom\. Reason\.*61, 1\-4 \(2018\), 367–422\.[https://doi\.org/10\.1007/S10817\-018\-9457\-5](https://doi.org/10.1007/S10817-018-9457-5)
- Charguéraud \(2016\)Arthur Charguéraud\. 2016\.Higher\-order representation predicates in separation logic\. In*Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20\-22, 2016*, Jeremy Avigad and Adam Chlipala \(Eds\.\)\. ACM, 3–14\.[https://doi\.org/10\.1145/2854065\.2854068](https://doi.org/10.1145/2854065.2854068)
- Charguéraud \(2020\)Arthur Charguéraud\. 2020\.Separation logic for sequential programs \(functional pearl\)\.*Proc\. ACM Program\. Lang\.*4, ICFP \(2020\), 116:1–116:34\.[https://doi\.org/10\.1145/3408998](https://doi.org/10.1145/3408998)
- Chen et al\.\(2015\)Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M\. Frans Kaashoek, and Nickolai Zeldovich\. 2015\.Using Crash Hoare logic for certifying the FSCQ file system\. In*Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, Monterey, CA, USA, October 4\-7, 2015*, Ethan L\. Miller and Steven Hand \(Eds\.\)\. ACM, 18–37\.[https://doi\.org/10\.1145/2815400\.2815402](https://doi.org/10.1145/2815400.2815402)
- Cohen et al\.\(2009\)Ernie Cohen, Markus Dahlweid, Mark A\. Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen, Wolfram Schulte, and Stephan Tobies\. 2009\.VCC: A Practical System for Verifying Concurrent C\. In*Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17\-20, 2009\. Proceedings**\(Lecture Notes in Computer Science, Vol\. 5674\)*, Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel \(Eds\.\)\. Springer, 23–42\.[https://doi\.org/10\.1007/978\-3\-642\-03359\-9\_2](https://doi.org/10.1007/978-3-642-03359-9_2)
- de Moura and Bjørner \(2008\)Leonardo Mendonça de Moura and Nikolaj S\. Bjørner\. 2008\.Z3: An Efficient SMT Solver\. In*Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29\-April 6, 2008\. Proceedings**\(Lecture Notes in Computer Science, Vol\. 4963\)*, C\. R\. Ramakrishnan and Jakob Rehof \(Eds\.\)\. Springer, 337–340\.[https://doi\.org/10\.1007/978\-3\-540\-78800\-3\_24](https://doi.org/10.1007/978-3-540-78800-3_24)
- Filliâtre and Paskevich \(2013\)Jean\-Christophe Filliâtre and Andrei Paskevich\. 2013\.Why3 \- Where Programs Meet Provers\. In*Programming Languages and Systems \- 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16\-24, 2013\. Proceedings**\(Lecture Notes in Computer Science, Vol\. 7792\)*, Matthias Felleisen and Philippa Gardner \(Eds\.\)\. Springer, 125–128\.[https://doi\.org/10\.1007/978\-3\-642\-37036\-6\_8](https://doi.org/10.1007/978-3-642-37036-6_8)
- Gordon \(2000\)Mike Gordon\. 2000\.From LCF to HOL: a short history\. In*Proof, Language, and Interaction, Essays in Honour of Robin Milner*, Gordon D\. Plotkin, Colin Stirling, and Mads Tofte \(Eds\.\)\. The MIT Press, 169–186\.
- Greenaway et al\.\(2012\)David Greenaway, June Andronick, and Gerwin Klein\. 2012\.Bridging the Gap: Automatic Verified Abstraction of C\. In*Interactive Theorem Proving \- Third International Conference, ITP 2012, Princeton, NJ, USA, August 13\-15, 2012\. Proceedings**\(Lecture Notes in Computer Science, Vol\. 7406\)*, Lennart Beringer and Amy P\. Felty \(Eds\.\)\. Springer, 99–115\.[https://doi\.org/10\.1007/978\-3\-642\-32347\-8\_8](https://doi.org/10.1007/978-3-642-32347-8_8)
- Greenaway et al\.\(2014\)David Greenaway, Japheth Lim, June Andronick, and Gerwin Klein\. 2014\.Don’t sweat the small stuff: formal verification of C code without the pain\. In*ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’14, Edinburgh, United Kingdom \- June 09 \- 11, 2014*, Michael F\. P\. O’Boyle and Keshav Pingali \(Eds\.\)\. ACM, 429–439\.[https://doi\.org/10\.1145/2594291\.2594296](https://doi.org/10.1145/2594291.2594296)
- Gruetter et al\.\(2024\)Samuel Gruetter, Viktor Fukala, and Adam Chlipala\. 2024\.Live Verification in an Interactive Proof Assistant\.*Proc\. ACM Program\. Lang\.*8, PLDI \(2024\), 1535–1558\.[https://doi\.org/10\.1145/3656439](https://doi.org/10.1145/3656439)
- Gu et al\.\(2016\)Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan \(Newman\) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo\. 2016\.CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels\. In*12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2\-4, 2016*, Kimberly Keeton and Timothy Roscoe \(Eds\.\)\. USENIX Association, 653–669\.[https://www\.usenix\.org/conference/osdi16/technical\-sessions/presentation/gu](https://www.usenix.org/conference/osdi16/technical-sessions/presentation/gu)
- Harrison \(2009\)John Harrison\. 2009\.HOL Light: An Overview\. In*Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17\-20, 2009\. Proceedings**\(Lecture Notes in Computer Science, Vol\. 5674\)*, Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel \(Eds\.\)\. Springer, 60–66\.[https://doi\.org/10\.1007/978\-3\-642\-03359\-9\_4](https://doi.org/10.1007/978-3-642-03359-9_4)
- Harrison et al\.\(2014\)John Harrison, Josef Urban, and Freek Wiedijk\. 2014\.History of Interactive Theorem Proving\.In*Computational Logic*, Jörg H\. Siekmann \(Ed\.\)\. Handbook of the History of Logic, Vol\. 9\. Elsevier, 135–214\.[https://doi\.org/10\.1016/B978\-0\-444\-51624\-4\.50004\-6](https://doi.org/10.1016/B978-0-444-51624-4.50004-6)
- Hoare et al\.\(2009\)C\. A\. R\. Hoare, Jayadev Misra, Gary T\. Leavens, and Natarajan Shankar\. 2009\.The verified software initiative: A manifesto\.*ACM Comput\. Surv\.*41, 4 \(2009\), 22:1–22:8\.[https://doi\.org/10\.1145/1592434\.1592439](https://doi.org/10.1145/1592434.1592439)
- Jacobs et al\.\(2011\)Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens\. 2011\.VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java\. In*NASA Formal Methods \- Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18\-20, 2011\. Proceedings**\(Lecture Notes in Computer Science, Vol\. 6617\)*, Mihaela Gheorghiu Bobaru, Klaus Havelund, Gerard J\. Holzmann, and Rajeev Joshi \(Eds\.\)\. Springer, 41–55\.[https://doi\.org/10\.1007/978\-3\-642\-20398\-5\_4](https://doi.org/10.1007/978-3-642-20398-5_4)
- Kirchner et al\.\(2015\)Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski\. 2015\.Frama\-C: A software analysis perspective\.*Formal Aspects Comput\.*27, 3 \(2015\), 573–609\.[https://doi\.org/10\.1007/S00165\-014\-0326\-7](https://doi.org/10.1007/S00165-014-0326-7)
- Klein et al\.\(2014\)Gerwin Klein, June Andronick, Kevin Elphinstone, Toby C\. Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser\. 2014\.Comprehensive formal verification of an OS microkernel\.*ACM Trans\. Comput\. Syst\.*32, 1 \(2014\), 2:1–2:70\.[https://doi\.org/10\.1145/2560537](https://doi.org/10.1145/2560537)
- Krebbers et al\.\(2017\)Robbert Krebbers, Amin Timany, and Lars Birkedal\. 2017\.Interactive proofs in higher\-order concurrent separation logic\. In*Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18\-20, 2017*, Giuseppe Castagna and Andrew D\. Gordon \(Eds\.\)\. ACM, 205–217\.[https://doi\.org/10\.1145/3009837\.3009855](https://doi.org/10.1145/3009837.3009855)
- Kumar et al\.\(2014\)Ramana Kumar, Magnus O\. Myreen, Michael Norrish, and Scott Owens\. 2014\.CakeML: a verified implementation of ML\. In*The 41st Annual ACM SIGPLAN\-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20\-21, 2014*, Suresh Jagannathan and Peter Sewell \(Eds\.\)\. ACM, 179–192\.[https://doi\.org/10\.1145/2535838\.2535841](https://doi.org/10.1145/2535838.2535841)
- Leinenbach and Santen \(2009\)Dirk Leinenbach and Thomas Santen\. 2009\.Verifying the Microsoft Hyper\-V Hypervisor with VCC\. In*FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2\-6, 2009\. Proceedings**\(Lecture Notes in Computer Science, Vol\. 5850\)*, Ana Cavalcanti and Dennis Dams \(Eds\.\)\. Springer, 806–809\.[https://doi\.org/10\.1007/978\-3\-642\-05089\-3\_51](https://doi.org/10.1007/978-3-642-05089-3_51)
- Leroy \(2009\)Xavier Leroy\. 2009\.Formal verification of a realistic compiler\.*Commun\. ACM*52, 7 \(2009\), 107–115\.[https://doi\.org/10\.1145/1538788\.1538814](https://doi.org/10.1145/1538788.1538814)
- Li et al\.\(2021\)Shih\-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, and John Zhuang Hui\. 2021\.A Secure and Formally Verified Linux KVM Hypervisor\. In*42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24\-27 May 2021*\. IEEE, 1782–1799\.[https://doi\.org/10\.1109/SP40001\.2021\.00049](https://doi.org/10.1109/SP40001.2021.00049)
- Mansky and Du \(2024\)William Mansky and Ke Du\. 2024\.An Iris Instance for Verifying CompCert C Programs\.*Proc\. ACM Program\. Lang\.*8, POPL \(2024\), 148–174\.[https://doi\.org/10\.1145/3632848](https://doi.org/10.1145/3632848)
- Memarian et al\.\(2016\)Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall, Robert N\. M\. Watson, and Peter Sewell\. 2016\.Into the depths of C: elaborating the de facto standards\. In*Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13\-17, 2016*, Chandra Krintz and Emery D\. Berger \(Eds\.\)\. ACM, 1–15\.[https://doi\.org/10\.1145/2908080\.2908081](https://doi.org/10.1145/2908080.2908081)
- Nipkow et al\.\(2002\)Tobias Nipkow, Lawrence C\. Paulson, and Markus Wenzel\. 2002\.*Isabelle/HOL \- A Proof Assistant for Higher\-Order Logic*\. Lecture Notes in Computer Science, Vol\. 2283\.Springer\.[https://doi\.org/10\.1007/3\-540\-45949\-9](https://doi.org/10.1007/3-540-45949-9)
- O’Hearn \(2019\)Peter W\. O’Hearn\. 2019\.Separation logic\.*Commun\. ACM*62, 2 \(2019\), 86–95\.[https://doi\.org/10\.1145/3211968](https://doi.org/10.1145/3211968)
- Project \(2024\)Android Open Source Project\. 2024\.Android Virtualization Architecture\.Avaiable on[https://source\.android\.com/docs/core/virtualization/architecture](https://source.android.com/docs/core/virtualization/architecture)\.
- Protzenko et al\.\(2020\)Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat\-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M\. Wintersteiger, and Santiago Zanella Béguelin\. 2020\.EverCrypt: A Fast, Verified, Cross\-Platform Cryptographic Provider\. In*2020 IEEE Symposium on Security and Privacy, SP 2020, San Francisco, CA, USA, May 18\-21, 2020*\. IEEE, 983–1002\.[https://doi\.org/10\.1109/SP40000\.2020\.00114](https://doi.org/10.1109/SP40000.2020.00114)
- Protzenko et al\.\(2017\)Jonathan Protzenko, Jean Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella Béguelin, Antoine Delignat\-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy\. 2017\.Verified low\-level programming embedded in F\*\.*Proc\. ACM Program\. Lang\.*1, ICFP \(2017\), 17:1–17:29\.[https://doi\.org/10\.1145/3110261](https://doi.org/10.1145/3110261)
- Pulte et al\.\(2023\)Christopher Pulte, Dhruv C\. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and Neel Krishnaswami\. 2023\.CN: Verifying Systems C Code with Separation\-Logic Refinement Types\.*Proc\. ACM Program\. Lang\.*7, POPL \(2023\), 1–32\.[https://doi\.org/10\.1145/3571194](https://doi.org/10.1145/3571194)
- Ramananandro et al\.\(2019\)Tahina Ramananandro, Antoine Delignat\-Lavaud, Cédric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, and Jonathan Protzenko\. 2019\.EverParse: Verified Secure Zero\-Copy Parsers for Authenticated Message Formats\. In*28th USENIX Security Symposium, USENIX Security 2019, Santa Clara, CA, USA, August 14\-16, 2019*, Nadia Heninger and Patrick Traynor \(Eds\.\)\. USENIX Association, 1465–1482\.[https://www\.usenix\.org/conference/usenixsecurity19/presentation/delignat\-lavaud](https://www.usenix.org/conference/usenixsecurity19/presentation/delignat-lavaud)
- Reynolds \(2002\)John C\. Reynolds\. 2002\.Separation Logic: A Logic for Shared Mutable Data Structures\. In*17th IEEE Symposium on Logic in Computer Science \(LICS 2002\), 22\-25 July 2002, Copenhagen, Denmark, Proceedings*\. IEEE Computer Society, 55–74\.[https://doi\.org/10\.1109/LICS\.2002\.1029817](https://doi.org/10.1109/LICS.2002.1029817)
- Rondon et al\.\(2008\)Patrick Maxim Rondon, Ming Kawaguchi, and Ranjit Jhala\. 2008\.Liquid types\. In*Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7\-13, 2008*, Rajiv Gupta and Saman P\. Amarasinghe \(Eds\.\)\. ACM, 159–169\.[https://doi\.org/10\.1145/1375581\.1375602](https://doi.org/10.1145/1375581.1375602)
- Sammler et al\.\(2021\)Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, and Deepak Garg\. 2021\.RefinedC: automating the foundational verification of C code with refined ownership types\. In*PLDI ’21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20\-25, 2021*, Stephen N\. Freund and Eran Yahav \(Eds\.\)\. ACM, 158–174\.[https://doi\.org/10\.1145/3453483\.3454036](https://doi.org/10.1145/3453483.3454036)
- Tao et al\.\(2021\)Runzhou Tao, Jianan Yao, Xupeng Li, Shih\-Wei Li, Jason Nieh, and Ronghui Gu\. 2021\.Formal Verification of a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware\. In*SOSP ’21: ACM SIGOPS 28th Symposium on Operating Systems Principles, Virtual Event / Koblenz, Germany, October 26\-29, 2021*, Robbert van Renesse and Nickolai Zeldovich \(Eds\.\)\. ACM, 866–881\.[https://doi\.org/10\.1145/3477132\.3483560](https://doi.org/10.1145/3477132.3483560)
- Xu et al\.\(2016\)Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang, and Zhaohui Li\. 2016\.A Practical Verification Framework for Preemptive OS Kernels\. In*Computer Aided Verification \- 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17\-23, 2016, Proceedings, Part II**\(Lecture Notes in Computer Science, Vol\. 9780\)*, Swarat Chaudhuri and Azadeh Farzan \(Eds\.\)\. Springer, 59–79\.[https://doi\.org/10\.1007/978\-3\-319\-41540\-6\_4](https://doi.org/10.1007/978-3-319-41540-6_4)
- Zhou et al\.\(2024\)Litao Zhou, Jianxing Qin, Qinshi Wang, Andrew W\. Appel, and Qinxiang Cao\. 2024\.VST\-A: A Foundationally Sound Annotation Verifier\.*Proc\. ACM Program\. Lang\.*8, POPL \(2024\), 2069–2098\.[https://doi\.org/10\.1145/3632911](https://doi.org/10.1145/3632911)