软件学报

作者：李希萌，王国辉，张倩颖，施智平，关永

单位：李希萌，首都师范大学 信息工程学院, 北京 100048;电子系统可靠性技术北京市重点实验室(首都师范大学), 北京 10004811,王国辉，首都师范大学 信息工程学院, 北京 100048;北京成像理论与技术高精尖创新中心(首都师范大学), 北京 10004802,张倩颖，首都师范大学 信息工程学院, 北京 100048;电子系统可靠性技术北京市重点实验室(首都师范大学), 北京 10004803,施智平，首都师范大学 信息工程学院, 北京 100048;电子系统可靠性技术北京市重点实验室(首都师范大学), 北京 10004804,关永，首都师范大学 信息工程学院, 北京 100048;北京成像理论与技术高精尖创新中心(首都师范大学), 北京 10004805

关键词：程序验证;大步操作语义;定理证明;Coq定理证明器

基金：国家重点研发计划(2019YFB1309900);国家自然科学基金(61876111,61877040,62002246);北京市教育委员会科技计划(KM201910028005,KM202010028010)

各类安全攸关系统的可靠运行离不开软件程序的正确执行. 程序的演绎验证技术为程序执行的正确性提供高度保障. 程序语言种类繁多, 且用途覆盖高可靠性场景的新式语言不断涌现, 难以为每种语言设计支撑其程序验证任务的整套逻辑规则, 并证明其相对于形式语义的可靠性和完备性. 语言无关的程序验证技术提供以程序语言的语义为参数的验证过程及其可靠性结果. 对每种程序语言, 提供其形式语义后可直接获得面向该语言的程序验证过程. 提出一种面向大步操作语义的语言无关演绎验证技术, 其核心是对不同语言中循环、递归等可导致无界行为的语法结构进行可靠推理的通用方法. 特别地, 借助大步操作语义的一种函数式形式化提供表达程序中子结构所执行计算的能力, 从而允许借助辅助信息对子结构进行推理. 证明所提出验证技术的可靠性和相对完备性, 通过命令式、函数式语言中的程序验证实例初步评估了该技术的有效性, 并在Coq辅助证明工具中形式化了所有理论结果和验证实例, 为基于辅助证明工具实现面向大步语义的语言无关程序验证工具提供了基础.

来源：2023年第8期

《软件学报》期刊编辑部

查看软件学报杂志2023年第8期