HELIX：面向LLVM IR的网络控制系统验证编译
编程语言
2026-04-22 v1
摘要
本文介绍HELIX的设计，这是一个以高性能和高保证数值计算为焦点的端到端验证代码生成系统。代码生成可针对广泛的计算机体系结构进行调优，以生成高效代码，同时提供对此类生成代码正确性的形式保证。以一个现实中的网络机器人系统为例，本文演示了如何使用HELIX，从高级数学公式出发，应用一系列针对中间语言的代数变换，生成高效的命令式实现。同时，在从原始公式到LLVM IR的形式语义保持性方面进行验证。我们用于高性能代码编译的方法是将向量和矩阵计算的代数变换转换为针对目标硬件上的并行或矢量化处理优化的数据流。用于形式化和验证此技术的抽象是一种运算语言及其语义保持的项重写。我们使用稀疏向量抽象表示部分计算，使我们能够使用代数推理证明并行分解属性。HELIX的验证基础设施包括多个中间语言和验证方法，全部在Coq证明助手中实现。特别是，它使用验证的项重写、翻译验证、元编程、验证编译和分层单子解释器；它还支持（经过验证的）数值分析的特定应用，正如我们通过本案例所示。
引用
@article{arxiv.2604.18593,
title = {HELIX: Verified compilation of cyber-physical control systems to LLVM IR},
author = {Vadim Zaliva and Yannick Zakowski and Ilia Zaichuk and Valerii Huhnin and Calvin Beck and Irene Yoon and Steve Zdancewic},
journal= {arXiv preprint arXiv:2604.18593},
year = {2026}
}