Algebraic Calculi for Separation Logic

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

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.