Los autores Yiyuan Cao, Jiayi Zhuang, Houjin Chen, Jinkai Fan, Wenbo Xu, Zhiyi Wang, Di Wang, Qinxiang Cao, Yingfei Xiong, Haiyan Zhao y Zhenjiang Hu presentan C*, un diseño de lenguaje con pruebas integradas para programación en C. C* extiende C con capacidades de verificación impulsadas por un motor de ejecución simbólica y un núcleo de prueba de estilo LCF. Permite la verificación en tiempo real al permitir a los programadores incrustar bloques de código de prueba junto al código de implementación, facilitando actualizaciones interactivas del estado actual de la prueba.

Su soporte de prueba expresivo y extensible permite a los usuarios construir bibliotecas reutilizables de definiciones lógicas, teoremas y automatización de pruebas programable. Crucialmente, C* unifica el desarrollo de código de implementación y de prueba al usar C como lenguaje común. El equipo implementó un prototipo y lo evaluó en un benchmark representativo de pequeños programas en C y un desafiante estudio de caso real: la función attach del asignador buddy de p KVM.

Los resultados demuestran que C* soporta la verificación de un amplio subconjunto de idiomas de programación en C y maneja eficazmente tareas de razonamiento complejas en escenarios reales.