 |
| |
|
[ people ] |
|
|
@ Bernhard Reus (PI)
@ 1 Research Fellow: Billiejoe Charlton
@ 2 PhD students Benjamin Horsfall and René Haberland
|
| |
|
[ summary ] |
|
Pointers are an important feature of programming languages used to define dynamically growing and recursive data structures. Many languages provide pointers not just to data but also functions or procedures, i.e. to executable code. Thus, code pointers offer high flexibility of code reconfiguration at runtime. Yet, their treatment in specification and verification has been poor due to their complexity. In order to write correct software in state-of-the-art languages it is paramount to have logics that permit reasoning about programs including function pointers.
It is important that reasoning about heaps is local and modular which means that verification can be simply done w.r.t. the part of the heap affected by code, and independently of other code modules linked at a later stage, respectively.
Separation Logic has presented us with a handle to tackle the complexity of pointers. It permits local reasoning on the heap, liberating the verifier from specifying and proving that most of the heap does not change when a procedure or command is executed.
The central objective of this project is to establish program (Hoare-) logics for languages with explicit and implicit code pointers making the benefits of Separation Logic amenable to them.
|
| |
|
[ duration ] |
|
November 2008 - October 2011
|
| |
|
[ publications ] |
|
J. Schwinghammer, L. Birkedal,
B. Reus, and H. Yang: Nested Hoare Triples and Frame Rules for
Higher-order Store, CSL'09 [pdf]
N.A. Charlton, B. Reus: A decidable class of verification conditions for programs with higher order store, AVOCS'09 [pdf]
|
| |
|
[ workplan ] |
|
A tentative Workplan for all team members including PhD students. This is subject to change but a good starting point. |
| |
|
[ further documents ] |
|
[ Royal Society | British Council |
EPSRC | Uni Grant Office ]
|
|
|
(EP/G003173/1)
