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

李希萌(1987-),男,博士,CCF专业会员,主要研究领域为形式化方法,软件验证;王国辉(1984-),男,博士,高级实验师,CCF专业会员,主要研究领域为形式化验证,高可靠嵌入式系统;张倩颖(1986-),女,博士,副教授,CCF专业会员,主要研究领域为形式化验证,系统安全,操作系统;施智平(1974-),男,博士,教授,博士生导师,CCF高级会员,主要研究领域为形式化方法,人工智能;关永(1966-),男,博士,教授,博士生导师,CCF专业会员,主要研究领域为形式化验证,高可靠嵌入式系统,机器人

通讯作者:

施智平,E-mail:shizp@cnu.edu.cn

中图分类号:

TP311

基金项目:

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


Unified Proof Technique for Iterative and Recursive Program Structures Based on Functional Semantics
Author:
  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [38]
  • |
  • 相似文献 [20]
  • | | |
  • 文章评论
    摘要:

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

    Abstract:

    The reliable functioning of safety-critical IT systems depends heavily on the correct execution of programs. Deductive program verification can be performed to guarantee the correct execution to a large extent. There are already a plethora of programming languages in use, and new languages oriented toward high-reliability scenarios are still being invented. As a result, it is difficult to devise a full-fledged logical system for each language to support the verification of programs and 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. This study proposes a language-independent verification technique based on big-step operational semantics. The technique features a unified procedure for sound reasoning about program structures that potentially cause unbounded behavior, such as iteration and recursion. In particular, the study employs a functional formalization of big-step operational 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. In addition, the study has proved the soundness and relative completeness of the proposed technique, evaluated the technique by verification examples in imperative and functional programming languages, and formalized all theoretical results and verification examples in the Coq proof assistant, and thus provides a basis for developing a language-independent program verifier with big-step operational semantics based on a proof assistant.

    参考文献
    [1] 王戟, 詹乃军, 冯新宇, 刘志明. 形式化方法概貌. 软件学报, 2019, 30(1): 33–61. http://www.jos.org.cn/1000-9825/5652.htm
    Wang J, Zhan NJ, Feng XY, Liu ZM. Overview of formal methods. Ruan Jian Xue Bao/Journal of Software, 2019, 30(1): 33–61 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5652.htm
    [2] Harrison J, Urban J, Wiedijk F. History of interactive theorem proving. Handbook of the History of Logic, 2014, 9: 135–214. [doi: 10.1016/B978-0-444-51624-4.50004-6]
    [3] Nielson HR, Nielson F. Semantics with Applications: An Appetizer. London: Springer, 2007.
    [4] 周巢尘, 詹乃军. 形式语义学引论. 第2版, 北京: 科学出版社, 2017.
    Zhou CC, Zhan NJ. Formal Semantics. 2nd ed., Beijing: Science Press, 2017 (in Chinese).
    [5] McCarthy J. Towards a mathematical science of computation. In: Proc. of the 1962 Information Processing Congress. 1962. 21–28.
    [6] Kirchner F, Kosmatov N, Prevosto V, Signoles J, Yakobowski B. Frama-C: A software analysis perspective. Formal Aspects of Computing, 2015, 27(3): 573–609. [doi: 10.1007/s00165-014-0326-7]
    [7] Ahrendt W, Beckert B, Bubel R, Hähnle R, Schmitt PH, Ulbrich M. Deductive Software Verification—The KeY Book: From Theory to Practice. Cham: Springer, 2016.
    [8] Filliâtre JC, Paskevich A. Why3—Where programs meet provers. In: Proc. of the 22nd European Symp. on Programming. Rome: Springer, 2013. 125–128.
    [9] Appel AW. Verified software toolchain. In: Proc. of the 20th European Symp. on Programming. Saarbrücken: Springer, 2011. 1–17.
    [10] Jung R, Krebbers R, Jourdan JH, Bizjak A, Birkedal L, Dreyer D. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 2018, 28: e20. [doi: 10.1017/S0956796818000151]
    [11] Moore JS. Inductive assertions and operational semantics. In: Proc. of the 12th IFIP WG 10.5 Advanced Research Working Conf. on Correct Hardware Design and Verification Methods. L’Aquila: Springer, 2003. 289–303.
    [12] Moore B, Peña L, Rosu G. Program verification by coinduction. In: Proc. of the 27th European Symp. on Programming. Thessaloniki: Springer, 2018. 589–618.
    [13] Stefănescu A, Park D, Yuwen SJ, Li YL, Roşu G. Semantics-based program verifiers for all languages. In: Proc. of the 2016 ACM SIGPLAN Int’l Conf. on Object-oriented Programming, Systems, Languages, and Applications. Amsterdam: ACM, 2016. 74–91.
    [14] Rosu G. K: A semantic framework for programming languages and formal analysis tools. In: Proc. of the 2017 Dependable Software Systems Engineering. IOS Press, 2017. 186–206.
    [15] Plotkin GD. A structural approach to operational semantics. Technical Report, Aarhus: Aarhus University, 1981.
    [16] Clément D, Despeyroux J, Despeyroux T, Kahn G. A simple applicative language: Mini-ML. In: Proc. of the 1986 ACM Conf. on LISP and Functional Programming. Cambridge: ACM, 1986. 13–27.
    [17] Hoare CAR. An axiomatic basis for computer programming. Communications of the ACM, 1969, 12(10): 576–580. [doi: 10.1145/363235.363259]
    [18] Dijkstra EW. Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM, 1975, 18(8): 453–457. [doi: 10.1145/360933.360975]
    [19] Bertot Y, Castéran P. Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Berlin: Springer, 2004.
    [20] Greenaway D. Automated proof-producing abstraction of C code [Ph.D. Thesis]. Sydney: University of New South Wales, 2015.
    [21] Bulwahn L, Krauss A, Haftmann F, Erkök L, Matthews J. Imperative functional programming with Isabelle/HOL. In: Proc. of the 21st Int’l Conf. on Theorem Proving in Higher Order Logics. Montreal: Springer, 2008. 134–149.
    [22] 张协力, 祝跃飞, 顾纯祥, 陈熹. C2P: 基于Pi演算的协议C代码形式化抽象方法和工具. 软件学报, 2021, 32(6): 1581–1596. http://www.jos.org.cn/1000-9825/6238.htm
    Zhang XL, Zhu YF, Gu CX, Chen X. C2P: Formal abstraction method and tool for C protocol code based on Pi caculus. Ruan Jian Xue Bao/Journal of Software, 2021, 32(6): 1581–1596 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/6238.htm
    [23] Reynolds JC. Separation logic: A logic for shared mutable data structures. In: Proc. of the 17th IEEE Symp. on Logic in Computer Science. Copenhagen: IEEE, 2002. 55–74.
    [24] Jones CB. Tentative steps toward a development method for interfering programs. ACM Transactions on Programming Languages and Systems, 1983, 5(4): 596–619. [doi: 10.1145/69575.69577]
    [25] Harel D, Kozen D, Tiuryn J. Dynamic Logic. Cambridge: MIT Press, 2000.
    [26] Benton N. Simple relational correctness proofs for static analyses and program transformations. In: Proc. of the 31st ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. Venice: ACM, 2004. 14–25.
    [27] Blazy S, Leroy X. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, 2009, 43(3): 263–288. [doi: 10.1007/s10817-009-9148-3]
    [28] Owens S, Myreen MO, Kumar R, Tan YK. Functional big-step semantics. In: Proc. of the 25th European Symp. on Programming. Eindhoven: Springer, 2016. 589–615.
    [29] 韩宁, 李希萌, 张倩颖, 王国辉, 施智平, 关永. 以太坊中间语言的可执行语义. 软件学报, 2021, 32(6): 1717–1732. http://www.jos.org.cn/1000-9825/6246.htm
    Han N, Li XM, Zhang QY, Wang GH, Shi ZP, Guan Y. Executable semantics of ethereum intermediate language. Ruan Jian Xue Bao/Journal of Software, 2021, 32(6): 1717–1732 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/6246.htm
    [30] Reyholds JC. Theories of Programming Languages. Cambridge: Cambridge University Press, 1998.
    [31] Cousot P, Cousot R. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. of the 4th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages. Los Angeles: ACM, 1977. 238–252.
    [32] Zhang FY, Nielson F, Nielson HR. Model checking as static analysis: Revisited. In: Proc. of the 9th Int’l Conf. on Integrated Formal Methods. Pisa: Springer, 2012. 99–112.
    [33] Schmidt D, Steffen B. Program analysis as model checking of abstract interpretations. In: Proc. of 5th Int’l Symp. on Static Analysis. Pisa: Springer, 1998. 351–380.
    [34] Ellison C, Rosu G. An executable formal semantics of C with applications. In: Proc. of the 39th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. Philadelphia: ACM, 2012. 533–544.
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

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

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

京公网安备 11040202500063号