Refining Existential Properties in Separation Logic Analyses

TL;DR

This paper introduces a CEGAR-like refinement method for separation logic analyses that detects and corrects spurious failures by refining the abstract domain to better capture existential properties such as list contents.

Contribution

It presents a novel approach combining abduction and domain refinement to improve the accuracy of separation logic program analyses for existential properties.

Findings

Effective detection of spurious failures in case studies

Refinement improves analysis accuracy for list properties

Demonstrated on real-world software like Redis and FreeRTOS

Abstract

In separation logic program analyses, tractability is generally achieved by restricting invariants to a finite abstract domain. As this domain cannot vary, loss of information can cause failure even when verification is possible in the underlying logic. In this paper, we propose a CEGAR-like method for detecting spurious failures and avoiding them by refining the abstract domain. Our approach is geared towards discovering existential properties, e.g. "list contains value x". To diagnose failures, we use abduction, a technique for inferring command preconditions. Our method works backwards from an error, identifying necessary information lost by abstraction, and refining the forward analysis to avoid the error. We define domains for several classes of existential properties, and show their effectiveness on case studies adapted from Redis, Azureus and FreeRTOS.