基于高阶模型检测的复杂高阶程序的验证方法研究

Model checking is an algorithmic technique that automatically checks whether a formal system satisfies some given modal logic property. The technique provides a powerful and fully automatic approach to verifying the correctness of programs. Verifying the program is challenging for modern languages like Java8, OCaml or C++11, since they support paradigms including concurrent, object-oriented and functional programming, which makes them inherently higher-order and complex. This brings new challenges to the traditional program verification methods. Higher-order model checking extends and subsumes traditional model checking techniques, and laid the foundation of verifying complex higher-order programs. Since the technique has not been effectively used to verify features of real-world programs, this project aims to conduct research on developing new methods for verifying complex higher-order programs by using and extending the higher-order model checking techniques. In particular, we plan to solve two major problems: 1) propose a new formal system to model complex higher-order programs that contain infinite data domain and multiple programming paradigms, by extending recursively-typed higher-order recursion schemes and by extending the theory of higher-order model checking; 2) present a well-defined model checking problem for the new system on safety properties and design sound and relatively-complete algorithms for the new problem. Finally, we will implement model checkers for the proposed algorithms and tools for verifying some Java8 and OCaml benchmark programs and conduct extensive experiments. We hope our research results in the project will provide new theory and techniques that help ensure the reliability of modern complex software applications.

模型检测是一种自动验证系统满足模态逻辑性质的算法技术，为验证程序正确性提供了有力工具。新一代程序语言如Java8、C++11等均为支持并发、函数式和面向对象等多种编程范式的复杂高阶程序，给传统程序验证方法提出了挑战。高阶模型检测扩展了传统模型检测，为验证复杂高阶程序奠定了理论基础。针对高阶模型检测尚不能有效地用于验证实际程序语言特点的现状，本项目将开展基于高阶模型检测技术的复杂高阶程序的验证方法研究。通过扩展高阶模型检测理论和算法，探索验证复杂高阶程序的新方法，并解决两个主要问题：1）扩展递归类型高阶文法和高阶模型检测理论以建模支持无限数据类型和多种编程范式的复杂高阶程序；2）为新系统提出验证安全性性质的良定性的模型检测问题，以及在理论上正确和相对完备的算法。此外，实现模型检测和程序验证原型工具，以Java8和OCaml程序语言子集为目标开展实例研究，为确保复杂软件系统可靠性提供新的理论和技术支持。

模型检测是一种自动验证系统满足模态逻辑性质的算法技术，为验证程序正确性提供了有力工具。新一代程序语言均为支持并发、函数式和面向对象等多种编程范式的复杂高阶程序，给传统程序验证方法提出了挑战。近年，函数式程序语言由于其安全、稳定等特性，越来越多地被用于区块链平台的有关开发中。高阶模型检测扩展了传统模型检测，为验证复杂高阶程序奠定了理论基础，在验证复杂高阶程序可靠性方面具有理论和应用价值。本项目研究基于高阶模型检测的复杂高阶程序的验证方法。通过深化和扩展高阶模型检测理论和算法技术，研究正确且相对完备的程序验证算法，包括为递归类型高阶模型检测研究提出正确且相对完备的饱和算法技术和原型工具，为条件下推模型检测子类模型研究提出固定参数多项式算法技术和原型工具等。此外，为自动合成递归函数式程序研究基于离线监督学习的算法技术和原型工具，与高阶程序验证互为补充，为确保复杂软件系统可靠性提供新的理论和技术支持。