Algebraic Calculi for 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.