Publication Type

Conference Paper

Version

acceptedVersion

Publication Date

4-2018

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.

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018), Thessaloniki, Greece, April 14-20

Identifier

10.1007/978-3-319-89960-2_3

Publisher

IEEE

City or Country

Thessaloniki, Greece

Additional URL

https://doi.org/10.1007/978-3-319-89960-2_3

Download

Share

COinS