Picture of virus

Open Access research that helps to deliver "better medicines"...

Strathprints makes available scholarly Open Access content by the Strathclyde Institute of Pharmacy and Biomedical Sciences (SIPBS), a major research centre in Scotland and amongst the UK's top schools of pharmacy.

Research at SIPBS includes the "New medicines", "Better medicines" and "Better use of medicines" research groups. Together their research explores multidisciplinary approaches to improve understanding of fundamental bioscience and identify novel therapeutic targets with the aim of developing therapeutic interventions, investigation of the development and manufacture of drug substances and products, and harnessing Scotland's rich health informatics datasets to inform stratified medicine approaches and investigate the impact of public health interventions.

Explore Open Access research by SIPBS. Or explore all of Strathclyde's Open Access research...

Amortised resource analysis with separation logic

Atkey, Robert (2010) Amortised resource analysis with separation logic. In: Proceedings of 19th European Symposium on Programming, ESOP 2010. Lecture Notes in Computer Science, 6012 . Springer, pp. 85-103.

[img]
Preview
PDF
amortised_sep_logic.pdf
Accepted Author Manuscript

Download (262kB) | Preview

Abstract

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.