33 citations · 42 across the 9 of their papers we have counts for
3 papers · 1 filter
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.…
Reasoning about Interior Mutability in Rust using Library-Defined Capabilities
Federico Poli, Xavier Denis, Peter Müller +1
Existing automated verification techniques for safe Rust code rely on the strong type-system properties to reason about programs, especially to deduce which memory locations do not…
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…