SEAL: Symbolic Execution with Separation Logic (Competition Contribution)

Tomáš Brablec, Tomáš Dacík, Tomáš Vojnar

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…