Output details
11 - Computer Science and Informatics
Queen Mary University of London
Output title
Automated Cyclic Entailment Proofs in Separation Logic.
Type
E - Conference contribution
Name of conference/published proceedings
CADE-23 - 23rd International Conference on Automated Deduction
Volume number
6803
Issue number
-
First page of article
131
ISSN of proceedings
-
Year of publication
2011
Number of additional authors
2
Additional information
<11>Separation logic is the basis for almost every modern automatic program verification tool for reasoning about dynamic-allocated data structures. Unfortunately, all such tools suffer due to inefficiency and imprecision of current entailment checkers. Although entailment checking is a fundamental issue for verification technology, an effective entailment procedure remains an open problem. This paper makes fundamental advances on this problem introducing new mechanisms able to automatically prove non-trivial inductive entailments unprovable with existing approaches. The technique developed here has already been implemented in the (freely available) open-source theorem prover Cyclist.
Interdisciplinary
-
Cross-referral requested
-
Research group
None
Citation count
0
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
