TY - GEN
T1 - Amortised resource analysis with separation logic
AU - Atkey, Robert
PY - 2010
Y1 - 2010
N2 - Type-based amortised resource analysis following Hofmann and Jost—where resources are associated with individual elements of data structures and doled out to the programmer under a linear typing discipline—have been successful in providing concrete resource bounds for functional programs, with good support for inference. In this work we translate the idea of amortised resource analysis to imperative languages by embedding a logic of resources, based on Bunched Implications, within Separation Logic. The Separation Logic component allows us to assert the presence and shape of mutable data structures on the heap, while the resource component allows us to state the resources associated with each member of the structure. We present the logic on a small imperative language with procedures and mutable heap, based on Java bytecode. We have formalised the logic within the Coq proof assistant and extracted a certified verification condition generator. We demonstrate the logic on some examples, including proving termination of in-place list reversal on lists with cyclic tails.
AB - Type-based amortised resource analysis following Hofmann and Jost—where resources are associated with individual elements of data structures and doled out to the programmer under a linear typing discipline—have been successful in providing concrete resource bounds for functional programs, with good support for inference. In this work we translate the idea of amortised resource analysis to imperative languages by embedding a logic of resources, based on Bunched Implications, within Separation Logic. The Separation Logic component allows us to assert the presence and shape of mutable data structures on the heap, while the resource component allows us to state the resources associated with each member of the structure. We present the logic on a small imperative language with procedures and mutable heap, based on Java bytecode. We have formalised the logic within the Coq proof assistant and extracted a certified verification condition generator. We demonstrate the logic on some examples, including proving termination of in-place list reversal on lists with cyclic tails.
KW - separation logic
KW - programming languages
UR - http://www.springerlink.com/content/x626l080j8037147/
UR - http://personal.cis.strath.ac.uk/~raa/amortised-sep-logic.html
U2 - 10.1007/978-3-642-11957-6_6
DO - 10.1007/978-3-642-11957-6_6
M3 - Conference contribution book
VL - 6012
T3 - Lecture Notes in Computer Science
SP - 85
EP - 103
BT - Proceedings of 19th European Symposium on Programming, ESOP 2010
A2 - Gordon, Andrew
PB - Springer
ER -