| 基于Isabelle定理证明器算法程序的形式化验证 |
| |
| 引用本文： | 游珍,薛锦云. 基于Isabelle定理证明器算法程序的形式化验证[J]. 计算机工程与科学, 2009, 31(10). DOI: 10.3969/j.issn.1007-130X.2009.10.024 |
| |
| 作者姓名： | 游珍 薛锦云 |
| |
| 作者单位： | 江西师范大学省高性能计算技术重点实验室,江西,南昌,330022;江西师范大学省高性能计算技术重点实验室,江西,南昌,330022;中国科学院软件研究所,北京,100190 |
| |
| 基金项目： | 国家自然科学基金资助项目,科技部国际科技合作资助项目 |
| |
| 摘 要： | 形式化验证对保证软件的正确性和可靠性具有十分重要的意义。定理机械证明是形式化验证的一个重要研究领域,Isabelle系统是一个被广泛运用的定理证明辅助工具。本文在分析Dijkstra最弱前置谓词理论的基础上,根据PAR方法开发的算法程序循环不变式,提出了一种使用Isabelle定理证明器对算法程序进行机械验证的方法。该方法既克服了传统手工验证过程的繁琐性和易错性等缺点,又达到提高验证效率和保证算法程序高可信的目标,具有很好的实用价值。
|
| 关 键 词： | 形式化验证 定理机械证明 Dijkstra最弱前置谓词理论 PAR方法 算法程序 定理证明器 |
Formal Verification of Algorithmic Programs Based on the Isabelle Theorem Prover |
| |
| YOU Zhen,XUE Jin-yun. Formal Verification of Algorithmic Programs Based on the Isabelle Theorem Prover[J]. Computer Engineering & Science, 2009, 31(10). DOI: 10.3969/j.issn.1007-130X.2009.10.024 |
| |
| Authors: | YOU Zhen XUE Jin-yun |
| |
| Abstract: | Formal verification plays an important role in ensuring software's correctness and dependability.Theorem's mechanical proof is a significant research domain of formal verification.The Isabelle system is generically considered as a useful tool for theorem proving.In this paper,according to the analysis of Dijkstra's weakest pre-condition theory and the algorithmic program's loop invariant developed by the PAR method,we offer a method of how to mechanically verify algorithmic programs based on Isabelle.The method not only overcomes the shortcomings of traditional manual verification,but also attains the goal of enhancing the dependability and efficiency of the verification process and ensuring the algorithmic programs' trustworthiness.Therefore,it is useful and valuable in practicability. |
| |
| Keywords: | formal verification theorem's mechanical proof Dijkstra's weakest pre-condition theory PAR method algorithmic program theorem prover |
| 本文献已被 万方数据 等数据库收录！ |
|
