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