Sound State Encodings in Translational Separation Logic Verifiers (Extended Version)

Hongyi Ling, Thibault Dardinier, Ellen Arlt +1

Automated program verifiers are often organized into a front-end, which encodes an input program into an intermediate verification language (IVL), and a back-end, which proves that…