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.

翻译：SEAL是一款用于验证操作无界链表数据结构的程序的静态分析器。该工具基于分离逻辑表示抽象内存状态，与其他基于分离逻辑的方法不同，SEAL采用通用分离逻辑求解器Astral进行可满足性与蕴涵关系判定，该求解器本身基于SMT转换实现。此设计形成了模块化架构，旨在便于扩展并与其他理论推理相结合。尽管仍处于原型阶段，SEAL在LinkedLists基础类别中取得了具有竞争力的结果，并且是仅有的四个能够验证无界链表程序的分析器之一。我们相信该工具的可扩展性结合后续开发，能够在未来竞赛中实现显著改进。