康烁

迪捷软件科技有限公司创始人&CEO

康烁，迪捷软件科技有限公司创始人，主持和参与了多个国内外开源项目，且在实际工程中均得到广泛应用。其中，SkyEye全数字实时仿真产品应用于国内航空航天领域的众多型号的研发测试领域；参与的开源项目L2C被国内核电单位应用于相关设备中。

议题：从模型到可执行程序的形式化验证：可信编译器l2c

在传统的软件开发过程中，编译器的错误往往被忽略。事实上，仅编译器自动测试工具Csmith（Xuejun Yang等）截至2011年2月，以及EMI/SPE（Zhendong Su等）截至2017年10月份，就发现了GCC和LLVM的共计近2000个“误编译”错误。这在安全攸关领域几乎是不可接受的。安全攸关系统的验证必须考虑编译器引入的错误，否则花大力气在源程序级的验证工作可能在目标程序级失效。在航空标准DO-178B/C中指出，在验证过程中应同等对待编译器与机载软件的验证。

L2C是一个把模型语言编译为C语言并经过形式化验证的开源编译器。它可以和compcert工具配合，从而保证模型语言翻译到二进制代码的整个过程是经过验证的，可信的。目前在安全攸关领域有较多应用。