3 papers
cs.PL2026
Hyper Separation Logic (extended version)
Trayan Gospodinov, Peter Müller, Thibault Dardinier
Many important functional and security properties--including non-interference, determinism, and generalized non-interference (GNI)--are hyperproperties, i.e., properties relating m…
cs.PL2026
Sound State Encodings in Translational Separation Logic Verifiers (Extended Version)
Hongyi Ling, Thibault Dardinier, Ellen Arlt +2
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…
cs.PL2024
Formal Foundations for Translational Separation Logic Verifiers (extended version)
Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy +2
Program verification tools are often implemented as front-end translations of an input program into an intermediate verification language (IVL) such as Boogie, GIL, Viper, or Why3.…