SEAL: Symbolic Execution with Separation Logic (Competition Contribution)

TL;DR

SEAL addresses memory-safety verification for programs that manipulate unbounded linked data structures by combining forward abstract interpretation over separation logic with a general-purpose solver Astral that translates SL to SMT. Its abstract domain represents memory as symbolic heaps of the form $∃ x_1, ..., x_m. ϕ_1 * ⋯ * ϕ_n$, enabling precise modeling of unbounded structures through inductive predicates, and its solver back-end ensures modular reasoning across theories. The work demonstrates competitive results in MemSafety-LinkedLists SVCOMP and highlights extensibility to data structures beyond SMGs through inductive predicates, while acknowledging current limitations such as partial language support and potential false positives from abstraction. Overall, SEAL offers a modular, extensible framework for memory-safety verification with a solver backend that can be evolved to cover richer data structures and languages.

Abstract

SEAL is a static analyser for the verification of programs that manipulate unbounded linked data structures. It is based on separation logic to represent abstract memory states and, unlike other separation-logic-based approaches, it employs a general-purpose separation logic solver Astral for satisfiability and entailment checking, which itself is based on translation to SMT. This design results in a modular architecture intended to be easier to extend and to combine with reasoning in other theories. Although still a prototype, SEAL achieved competitive results in the LinkedLists base category and was one of only four analysers capable of verifying programs with unbounded lists. We believe that the tool's extensibility, combined with further development, can lead to significant improvements in future competitions.