Ilya Sergey

Lazy Proof Automation for Separation Logic

2026 · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics)

Separation Logic is an established formalism for deductive verification of heap-manipulating programs. Proofs of symbolic heap entailment, an analogue of the ordinary logical implication, are amongst the most common reasoning steps in Separation Logic, and …