@inproceedings{b1126c2c2bcf47dd87a947441edf27b0,
title = "Frame inference for inductive entailment proofs in separation logic",
abstract = "Given separation logic formulae A and C, frame inference is the problem of checking whether A entails C and simultaneously inferring residual heaps. Existing approaches on frame inference do not support inductive proofs with general inductive predicates. In this work, we present an automatic frame inference approach for an expressive fragment of separation logic. We further show how to strengthen the inferred frame through predicate normalization and arithmetic inference. We have integrated our approach into an existing verification system. The experimental results show that our approach helps to establish a number of non-trivial inductive proofs which are beyond the capability of all existing tools.",
author = "Le, {Quang Loc} and Jun Sun and Shengchao Qin",
year = "2018",
month = apr,
day = "12",
doi = "10.1007/978-3-319-89960-2_3",
language = "English",
isbn = "9783319899596",
series = "Lecture Notes in Computer Science",
publisher = "Springer Open",
pages = "41--60",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
address = "United Kingdom",
note = "24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems : Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, TACAS 2018 ; Conference date: 14-04-2018 Through 20-04-2018",
}