Algebraic Calculi for Separation Logic

分离逻辑的代数演算

• 批准号: 188417285
• 负责人: Professor Dr. Bernhard Möller
• 金额: --
• 依托单位: Institut für Informatik
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2011
• 资助国家: 德国
• 起止时间: 2010-12-31 至 2014-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/188417285?language=en
• 关键词: Algebraic; Calculi; Separation; Logic

For about 40 years there have been investigations how to ensure correctness of programs by strictly formal methods. Since the calculi by Hoare and Dijkstra do not provide constructs for dealing with complex data structures, in particular those involving pointers, they have recently been extended by Reynolds, O Hearn and others into separation logic. By now this also incorporates aspects of concurrency and of shared mutable data structures. Special-purpose theorem provers support the verification tasks of these calculi. A disadvantage of such an approach is that for each calculus a new prover has to be developed. This approach is cumbersome, expensive and time-consuming.Here the idea of algebraisation enters. It frequently allows, by abstraction, formal reasoning using simple equational laws as known from school algebra. These can directly be entered into existing fully automatic theorem provers, and there is no need to construct proof systems anew for every problem domain. The goal of the project is to develop, using already existingbasic theories, an algebraic representation of separation logics. Particular attention is paid to characterising separation logic algebraically and to verifying properties using the algebra. The positive side-effect that algebraisation allows using existing theorem provers will lead to anautomation of verification tasks.

大约40年来，人们一直在研究如何通过严格的正式方法来确保程序的正确性。由于Hoare和Dijkstra的演算没有提供处理复杂数据结构的构造，特别是那些涉及指针的数据结构，它们最近被Reynolds、O Hain和其他人扩展到分离逻辑中。到目前为止，这还包含了并发性和共享可变数据结构的各个方面。专用定理证明器支持这些演算的验证任务。这种方法的一个缺点是，对于每个微积分，都必须开发一个新的证明器。这种方法繁琐、昂贵、耗时。代数化的想法就是在这里进入的。它经常允许通过抽象，使用学校代数中已知的简单方程定律进行形式推理。这些都可以直接输入到现有的全自动定理证明器中，而不需要为每个问题域重新构建证明系统。该项目的目标是利用已经存在的基本理论，开发分离逻辑的代数表示。特别注意分离逻辑的代数刻画和使用该代数来验证性质。代数化允许使用现有定理证明器的积极副作用将导致验证任务的自动化。

项目成果

Developments in concurrent Kleene algebra

• DOI: 10.1007/978-3-319-06251-8_1
• 发表时间: 2014-04
• 期刊: J. Log. Algebraic Methods Program.
• 作者: T. Hoare;S. Staden;B. Möller;G. Struth;Jules Villard;Huibiao Zhu;P. O'Hearn

Abstract Dynamic Frames

抽象动态框架

• DOI: 10.1007/978-3-319-06251-8_10
• 发表时间: 2014
• 作者: Han-Hing Dang: Abstract Dynamic Frames

Extended transitive separation logic

• DOI: 10.1016/j.jlamp.2014.12.002
• 发表时间: 2015-05
• 期刊: J. Log. Algebraic Methods Program.
• 作者: Han-Hing Dang;B. Möller

Modal algebra and Petri nets

模态代数和 Petri 网

• DOI: 10.1007/s00236-015-0216-3
• 发表时间: 2015
• 期刊: Acta Informatica
• 影响因子: 0.6
• 作者: H.-H. Dang;B. Möller
• 通讯作者: B. Möller

Exploring an Interface Model for CKA

• DOI: 10.1007/978-3-319-19797-5_1
• 发表时间: 2015-06
• 作者: B. Möller;Tony Hoare