UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

Automated cyclic entailment proofs in separation logic

Brotherston, J; Distefano, D; Petersen, RL; (2011) Automated cyclic entailment proofs in separation logic. In: (pp. pp. 131-146).

Full text not available from this repository.


We present a general automated proof procedure, based upon cyclic proof, for inductive entailments in separation logic. Our procedure has been implemented via a deep embedding of cyclic proofs in the HOL Light theorem prover. Experiments show that our mechanism is able to prove a number of non-trivial entailments involving inductive predicates. © 2011 Springer-Verlag Berlin Heidelberg.

Type: Proceedings paper
Title: Automated cyclic entailment proofs in separation logic
ISBN-13: 9783642224379
DOI: 10.1007/978-3-642-22438-6_12
UCL classification: UCL > School of BEAMS
UCL > School of BEAMS > Faculty of Engineering Science
URI: http://discovery.ucl.ac.uk/id/eprint/1363364
Downloads since deposit
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item