Les auteurs Yiyuan Cao, Jiayi Zhuang, Houjin Chen, Jinkai Fan, Wenbo Xu, Zhiyi Wang, Di Wang, Qinxiang Cao, Yingfei Xiong, Haiyan Zhao et Zhenjiang Hu présentent C*, une conception de langage intégrant la preuve pour la programmation en C. C* étend C avec des capacités de vérification alimentées par un moteur d'exécution symbolique et un noyau de preuve de style LCF. Il permet la vérification en temps réel en permettant aux programmeurs d'intégrer des blocs de code de preuve aux côtés du code d'implémentation, facilitant les mises à jour interactives de l'état de preuve actuel.

Son support de preuve expressif et extensible permet aux utilisateurs de construire des bibliothèques réutilisables de définitions logiques, de théorèmes et d'automatisation de preuve programmable. Crucialement, C* unifie le développement du code d'implémentation et du code de preuve en utilisant C comme langage commun. L'équipe a implémenté un prototype et l'a évalué sur un benchmark représentatif de petits programmes C et une étude de cas réelle difficile : la fonction attach de l'allocateur buddy de p KVM.

Les résultats démontrent que C* prend en charge la vérification d'un large sous-ensemble d'idiomes de programmation C et gère efficacement des tâches de raisonnement complexes dans des scénarios réels.