SEAL: Symbolic Execution with Separation Logic (Competition Contribution)

TL;DR

SEAL is a modular static analysis tool using separation logic and SMT solving to verify programs manipulating unbounded linked data structures, demonstrating competitive performance in verification tasks.

Contribution

It introduces a flexible, extensible separation logic-based verifier employing a general-purpose solver, improving modularity and potential for integration with other reasoning methods.

Findings

Achieved competitive results in verifying unbounded linked data structures.

Successfully verified programs with unbounded lists.

Demonstrated modular architecture for easier extension and integration.

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.