6 citations · 7 across the 4 of their papers we have counts for
4 papers · 1 filter
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…
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…
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.…
Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version)
Gaurav Parthasarathy, Thibault Dardinier, Benjamin Bonneau +2
Automated program verifiers are typically implemented using an intermediate verification language (IVL), such as Boogie or Why3. A verifier front-end translates the input program a…