SEAL: Symbolic Execution with Separation Logic (Competition Contribution)
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866915779622993920 |
|---|---|
| author | Brablec, Tomáš Dacík, Tomáš Vojnar, Tomáš |
| author_facet | Brablec, Tomáš Dacík, Tomáš Vojnar, Tomáš |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_05703 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | SEAL: Symbolic Execution with Separation Logic (Competition Contribution) Brablec, Tomáš Dacík, Tomáš Vojnar, Tomáš Software Engineering 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. |
| title | SEAL: Symbolic Execution with Separation Logic (Competition Contribution) |
| topic | Software Engineering |
| url | https://arxiv.org/abs/2602.05703 |