Output details
11 - Computer Science and Informatics
Queen Mary University of London
Automated Cyclic Entailment Proofs in Separation Logic.
<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.