权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Cyclic Proofs for Logic-Based Program Verification

基于逻辑的程序验证的循环证明

基本信息

批准号：
EP/F043767/1
负责人：
James Brotherston
金额：
$ 32.29万
依托单位：
Imperial College London
依托单位国家：
英国
项目类别：
Fellowship
财政年份：
2008
资助国家：
英国
起止时间：
2008 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FF043767%2F1
关键词：
Cyclic Proofs Logic Based Program

项目摘要

The last few years have seen a increasingly widespreadinterest, both from the academic perspective and from elementsof industry, in the mathematical verification of desirableproperties of computer programs. Such properties might state,for example, that a program does not exceed its memory bounds(``memory safety'') or that it is always able to perform acertain action (``liveness''). The development of appropriatereasoning principles for programs and of proof systems andcomputer tools supporting those principles is thus currentlyattracting considerable activity amongst the computer scienceresearch community.Despite the advances in developing various forms of programlogic, the underlying notion of a *proof* of a programproperty has changed very little; by default, a proof is afinite tree whose construction respects the particularinference rules of the logic (a.k.a. derivation tree ), sothat the leaves of the tree are axiom instances and the root ofthe tree is the theorem to be proven, with intermediate nodesrelated by logical inferences. Recently, however, analternative mode of formal proof has been mooted as a paradigmfor reasoning in logics that feature various forms ofrecursion, known as *cyclic proof*. A cyclic proof isessentially obtained by identifying some cycles in a derivationtree, i.e., a cyclic proof is really a regular, infinitederivation tree, represented in cyclic graph form. Typically,not every such proof structure represents a sound proof, so anadditional, global guardedness condition is imposed oncyclic proofs that ensures their soundness. The existing investigations of cyclic proof, first in the purelogical settings of first-order logic and BI with inductivedefinitions, and subsequently in a separation logic systemfor proving termination of simple programs, have demonstratedits viability as a tool for formal reasoning, and its potentialpower as a proof method. Moreover, in the case of first-orderlogic with inductive definitions, a completeness result foran associated infinitary proof system establishes the semanticnaturality of the approach. We view our previous work in thesedirections as having substantially established the area ofcyclic proof as both a theoretically natural one worthy ofstudy, and ripe for applications in program verification.The broad aim of the proposed Postdoctoral Fellowship is tobuild on the developed theoretical foundations of cyclic proof,and especially its initial development into separationlogic-based reasoning about programs, in order to furtherexploit the ideas in the direction of applications. First, we wish to formulate and analyse cyclic proof systems for program verification based on separation logic, and to extend the cyclic proof concept to mixed induction and coinduction. Second, we wish to investigate the potential of cyclic proof as a vehicle for automated theorem proving.

在过去的几年里，无论是从学术的角度还是从工业的角度，人们对计算机程序的可验证性的数学验证都越来越感兴趣。例如，这样的属性可以声明程序没有超出它的内存限制（"内存安全“），或者它总是能够执行某个操作（"活动”）。因此，为程序开发适当的推理原则，并开发支持这些原则的证明系统和计算机工具，目前在计算机科学研究界引起了相当大的兴趣。尽管在开发各种形式的程序逻辑方面取得了进展，但程序属性的证明的基本概念几乎没有改变;默认情况下，证明是一个有限的树，它的构造遵循逻辑的特定推理规则（也称为“逻辑推理”）。导出树），这样树的叶子是公理实例，树的根是要证明的定理，中间节点由逻辑推理联系起来。然而，最近，一种形式证明的替代模式被提出来作为逻辑推理的范例，这种逻辑推理以各种形式的递归为特征，被称为循环证明。一个循环证明实质上是通过在一个导子树中识别一些循环来获得的，即，一个循环证明实际上是一个规则的无限导出树，用循环图的形式表示。通常，并不是每个这样的证明结构都代表一个可靠的证明，所以一个额外的全局保护条件被强加在循环证明上，以确保它们的可靠性。循环证明的现有研究，首先是在一阶逻辑和BI的纯逻辑设置与归纳定义，随后在分离逻辑系统证明简单程序的终止性，已经证明了它作为形式化推理工具的可行性，以及它作为证明方法的潜在力量。此外，在具有归纳定义的一阶逻辑的情况下，一个相关的无穷证明系统的完备性结果建立了该方法的语义自然性。我们认为我们以前在这些方向上的工作已经基本上建立了循环证明领域，作为一个理论上自然的值得研究的领域，并且在程序验证中的应用已经成熟。拟议的博士后奖学金的广泛目标是建立在循环证明的发展理论基础上，特别是它最初的发展成为基于分离逻辑的程序推理，以便在应用方向上进一步开拓思路。首先，我们希望制定和分析基于分离逻辑的程序验证循环证明系统，并将循环证明概念扩展到混合归纳和共归纳。第二，我们希望研究循环证明作为自动定理证明工具的潜力。