Automated cyclic entailment proofs in separation logic.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
(pp. 131 - 146).
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.
|Title:||Automated cyclic entailment proofs in separation logic|
|UCL classification:||UCL > School of BEAMS > Faculty of Engineering Science > Computer Science|
Archive Staff Only