6 citations · 11 across the 5 of their papers we have counts for
5 papers
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…
Verification-Preserving Inlining in Automatic Separation Logic Verifiers (extended version)
Thibault Dardinier, Gaurav Parthasarathy, Peter Müller
Bounded verification has proved useful to detect bugs and to increase confidence in the correctness of a program. In contrast to unbounded verification, reasoning about calls via (…
Sound Automation of Magic Wands (extended version)
Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks +2
The magic wand (also called separating implication) is a separation logic connective commonly used to specify properties of partial data structures, for instance…
Formally Validating a Practical Verification Condition Generator (extended version)
Gaurav Parthasarathy, Peter Müller, Alexander J. Summers
A program verifier produces reliable results only if both the logic used to justify the program's correctness is sound, and the implementation of the program verifier is itself cor…