Gaurav Parthasarathy

Hi, I am a software engineer at Veezoo. I enjoy developing trustworthy software.

I recently completed my PhD in computer science at ETH Zurich under the supervision of Peter Müller (main advisor) and Alex Summers. In my PhD, I developed techniques for formally verifying the correctness of automatic program verifiers, which are tools that automatically check whether programs do not have any bugs. In short: I verified verifiers. A distinguishing aspect of my research is that it targets implementations of automatic program verifiers used in practice.

Research Publications

Formal Foundations for Translational Separation Logic Verifiers
Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, Peter Müller
2025 Principles of Programming Languages (POPL)
[pdf] [publisher] [extended version]
Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language
Gaurav Parthasarathy, Thibault Dardinier, Benjamin Bonneau, Peter Müller, Alexander J. Summers
2024 Programming Language Design and Implementation (PLDI)
[pdf] [publisher] [extended version]
Verification-Preserving Inlining in Automatic Separation Logic Verifiers
Thibault Dardinier, Gaurav Parthasarathy, Peter Müller
2023 Object-Oriented Programming, Systems, Languages & Applications (OOPSLA)
[pdf] [publisher] [extended version]
Sound Automation of Magic Wands
Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Peter Müller, Alexander J. Summers
2022 Computer Aided Verification (CAV)
[pdf] [publisher] [extended version]
Formally Validating a Practical Verification Condition Generator
Gaurav Parthasarathy, Peter Müller, Alexander J. Summers
2021 Computer Aided Verification (CAV)
[pdf] [publisher] [extended version]
The Future is Ours: Prophecy Variables in Separation Logic
Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, Bart Jacobs
2020 Principles of Programming Languages (POPL)
[pdf] [publisher]

Dissertation

Formally Validating Translational Program Verifiers
Final version submitted and accepted in December 2024 (defended in November 2024)
[pdf] [doi]

Talks

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language
2024 PLDI conference in Copenhagen, Denmark
Making the Boogie Verifier Foundational
2024 Swiss Verification Day in Neuchâtel, Switzerland
Formally Validating a Practical Verification Condition Generator
2021 CAV conference virtually