Frame inference for inductive entailment proofs in separation logic

Quang Loc Le, Jun Sun, Shengchao Qin

Research output: Chapter in Book/Report/Conference proceedingConference contribution

128 Downloads (Pure)

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.

Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication24th International Conference, TACAS 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018 Thessaloniki, Greece, April 14 – 20, 2018 Proceedings, Part I
PublisherSpringer Open
Pages41-60
Number of pages20
ISBN (Electronic)9783319899602
ISBN (Print)9783319899596
DOIs
Publication statusPublished - 12 Apr 2018
Event24th 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 - Thessaloniki, Greece
Duration: 14 Apr 201820 Apr 2018

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Nature
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Abbreviated titleTACAS 2018
CountryGreece
CityThessaloniki
Period14/04/1820/04/18

Profiles

Cite this

Le, Q. L., Sun, J., & Qin, S. (2018). Frame inference for inductive entailment proofs in separation logic. In Tools and Algorithms for the Construction and Analysis of Systems: 24th International Conference, TACAS 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018 Thessaloniki, Greece, April 14 – 20, 2018 Proceedings, Part I (pp. 41-60). (Lecture Notes in Computer Science). Springer Open. https://doi.org/10.1007/978-3-319-89960-2_3