Le, Quang Loc; Le, Xuan-Bach D; (2023) An Efficient Cyclic Entailment Procedure in a Fragment of Separation Logic. In: International Conference on Foundations of Software Science and Computation Structures FoSSaCS 2023: Foundations of Software Science and Computation Structures. (pp. pp. 477-497). Springer, Cham

Text Le_978-3-031-30829-1.pdf Download (0B)

Abstract

An efficient entailment proof system is essential to compositional verification using separation logic. Unfortunately, existing decision procedures are either inexpressive or inefficient. For example, Smallfoot is an efficient procedure but only works with hardwired lists and trees. Other procedures that can support general inductive predicates run exponentially in time as their proof search requires back-tracking to deal with a disjunction in the consequent. This paper presents a decision procedure to derive cyclic entailment proofs for general inductive predicates in polynomial time. Our procedure is efficient and does not require back-tracking; it uses normalisation rules that help avoid the introduction of disjunction in the consequent. Moreover, our decidable fragment is sufficiently expressive: It is based on compositional predicates and can capture a wide range of data structures, including sorted and nested list segments, skip lists with fast-forward pointers, and binary search trees. We implemented the proposal in a prototype tool, called S2SLin , and evaluated it over challenging problems from a recent separation logic competition. The experimental results confirm the efficiency of the proposed system.

Download activity - last month

Export as XMLJSONCSV

Download activity - last 12 months

Export as CSVJSONXML

Downloads by country - last 12 months

Export as XMLJSONCSV

Archive Staff Only

View Item