Imperial College London
Alternate

ProfessorPhilippaGardner

Faculty of Engineering, Department of Computing

Professor of Theoretical Computer Science
 
 
 
//

Contact

 

+44 (0)20 7594 8292p.gardner Website

 
 
//

Location

 

453Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@techreport{Ntzik:2015,
author = {Ntzik, G and da, Rocha Pinto P and Gardner, P},
publisher = {Department of Computing, Imperial College London},
title = {Fault-tolerant Resource Reasoning (Extended Version)},
url = {http://www.doc.ic.ac.uk/},
year = {2015}
}
Download

RIS format (EndNote, RefMan)

TY  - RPRT
AB  - Separation logic has been successful at verifying that programs do not crash due to illegal use of resources. The underlying assumption, however, is that machines do not fail. In practice, machines can fail unpredictably for various reasons, e.g. power loss, corrupting resources. Critical software, e.g. file systems, employ recovery methods to mitigate these effects. We introduce an extension of the Views framework to reason about such methods. We use concurrent separation logic as an instance of the framework to illustrate our reasoning, and explore programs using write-ahead logging, e.g. an ARIES recovery algorithm.
AU  - Ntzik,G
AU  - da,Rocha Pinto P
AU  - Gardner,P
PB  - Department of Computing, Imperial College London
PY  - 2015///
TI  - Fault-tolerant Resource Reasoning (Extended Version)
UR  - http://www.doc.ic.ac.uk/
UR  - http://hdl.handle.net/10044/1/26153
ER  -
Download