Os autores Yiyuan Cao, Jiayi Zhuang, Houjin Chen, Jinkai Fan, Wenbo Xu, Zhiyi Wang, Di Wang, Qinxiang Cao, Yingfei Xiong, Haiyan Zhao e Zhenjiang Hu apresentam C*, um design de linguagem com prova integrada para programação em C. C* estende C com capacidades de verificação alimentadas por um motor de execução simbólica e um kernel de prova de estilo LCF. Permite verificação em tempo real ao permitir que programadores insiram blocos de código de prova junto ao código de implementação, facilitando atualizações interativas do estado atual da prova.

Seu suporte de prova expressivo e extensível permite que usuários construam bibliotecas reutilizáveis de definições lógicas, teoremas e automação de prova programável. Crucialmente, C* unifica o desenvolvimento de código de implementação e de prova ao usar C como linguagem comum. A equipe implementou um protótipo e o avaliou em um benchmark representativo de pequenos programas em C e um estudo de caso real desafiador: a função attach do alocador buddy do p KVM.

Os resultados demonstram que C* suporta a verificação de um amplo subconjunto de idiomas de programação em C e lida efetivamente com tarefas de raciocínio complexas em cenários reais.