跨语言功能一致性验证方法、装置、存储介质及程序产品

本发明提供一种跨语言功能一致性验证方法、装置、存储介质及程序产品，该方法包括：将待验证第一语言代码编译为中间表示的第一格式文件，基于预定形式化验证语言建模，生成第一形式化规范；将第二语言代码编译为中间表示的第二格式文件，建模生成第二形式化规范；使用形式化验证工具通过符号执行验证第一格式文件和第一形式化验证语言规范的一致性，以及第二格式文件和第二形式化验证语言规范的一致性；在二者均一致的情况下，通过形式化验证工具验证第一形式化验证语言规范和第二形式化验证语言规范的等价性。本发明能够解决传统的功能一致性验证方法，无法证明不同语言实现的代码在所有输入条件下都保持等价的问题，能够提升验证效率和完备性。