Algebraic Calculi for Separation Logic

Start date: 01.04.2011
Duration: 2 years
Funded by: DFG (Deutsche Forschungsgemeinschaft)
Local head of project: Prof. Dr. Bernhard Möller
Local scientists: Han-Hing Dang
External scientists / cooperations: Sir Tony Hoare (Microsoft Research)
Prof. Dr. Georg Struth (University of Sheffield)
John Wickerson (Computer Laboratory, University of Cambridge)
Prof. Peter O'Hearn (Queen Mary, University of London)
Rasmus Lerchedahl Petersen (Queen Mary, University of London)
Dr. Peter Höfner (NICTA Australia)
Publications: Publication list


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 existing basic 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 an automation of verification tasks.