基于函数式语义的循环和递归程序结构通用证明技术
作者:
作者单位:

作者简介:

通讯作者:

施智平,shizp@cnu.edu.cn

中图分类号:

TP311

基金项目:

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


A Unified Proof Technique for Iterative and Recursive Program Structures based on Functional Semantics
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    The reliable functioning of safety-critical IT systems depends heavily on the correct execution of program code. Deductive program verification can be performed to provide a high level of correctness guarantees for computer programs. There is a plethora of different programming languages in use, and new languages oriented for high reliability scenarios are still being invented. It can be difficult to devise for each such language a full-fledged logical system supporting the verification of programs, and to prove the soundness and completeness of the logical system with respect to the formal semantics of the language. Language-independent verification techniques offer sound verification procedures parameterized over the formal semantics of programming languages. The specialization of the verification procedure with the formal semantics of a concrete programming language directly gives rise to a verification procedure for the language. In this article, we propose a language-independent verification technique based on big-step operational semantics. The technique features a unified procedure for the sound reasoning about program structures that potentially causes unbounded behavior, such as iteration and recursion. In particular, we employ a functional formalization of big-step semantics to support the explicit representation of the computation performed by the sub-structures of a program. This representation enables the exploitation of the auxiliary information provided for these sub-structures in the unified reasoning process. We prove the soundness and relative completeness of the proposed technique, evaluate the technique using verification examples in imperative and functional programming languages, and mechanize all the formal results and verification examples in the Coq proof assistant. The development provides a basis for the implementation of a language-independent program verifier in a proof assistant based on big-step operational semantics.

    参考文献
    相似文献
    引证文献
引用本文

李希萌,王国辉,张倩颖,施智平,关永.基于函数式语义的循环和递归程序结构通用证明技术.软件学报,,():0

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2021-09-04
  • 最后修改日期:2022-01-10
  • 录用日期:
  • 在线发布日期: 2022-03-24
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号