Viper Roots
Formal Foundations of Translational Verifiers
This project aims at providing formal foundations for the Viper verification infrastructure and similar verification tools. This effort includes developing a formal semantics for Viper and extending the Viper verifier to produce certificates for successful verification attempts - self-contained proofs that can be checked by independent tools.
Analogous to the architecture of compilers, many verification tools are implemented as a sequence of translation steps from programs and specifications to proof obligations in a suitable logic. Proof obligations in such translational verifiers are often expressed via intermediate verification languages (IVL). The IVL of a translational verifier decouples the front-end (which encodes the semantics of the input program) from the back-end (which automates the proof search). Thus, back-ends can be re-used across many verifiers, which drastically reduces the effort of building verifiers and facilitates the use of a portfolio of reasoning approaches. Examples of translational verifiers include Prusti (for Rust), Nagini (for Python), Gobra (for Go), and external pageVerCorscall_made (for Java) based on the Viper IVL, external pageCorralcall_made and external pageDafnycall_made based on the external pageBoogie IVLcall_made, as well as external pageFrama-Ccall_made (for C) and external pageKrakatoacall_made (for Java) based on the external pageWhy3 IVLcall_made.
Our goal is to increase the reliability of translational verifiers. To guarantee correctness of a translational verifier, one must guarantee correctness of its underlying logic justifying the translations, as well as the implementation of the verifier itself, which often consists of multiple thousands of lines of code. To address these points, we aim to find solutions to the following challenges: (1) The development of a meta-theoretical framework for soundness proofs justifying the verifier translations, and (2) the automatic generation of foundational proofs that reduce the trusted code base of translational verifier implementations.
To enable solutions for both of these challenges, a formal semantics for the IVL used in the translational verifier is required. The development of such a semantics is non-trivial for the Viper IVL, which can directly express resources via permissions in the style of separation logic. For instance, Viper supports the manipulation and inspection of permissions, which can lead to subtle errors in program verifiers when applying standard techniques such as method inlining without additional checks. As part of our efforts, we aim to give a formal semantics for Viper and to solve the challenges outlined above for translational verifiers based on Viper. We formalize our results in the Isabelle/HOL theorem prover.
Project Members
Thibault Dardinier
Peter Müller
Gaurav Parthasarathy
external pageAlex Summercall_made (UBC)
Key Publications
- T. Dardinier, G. Parthasarathy, and P. Müller: Verification-Preserving Inlining in Automatic Separation Logic Verifiers
Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), Proc. ACM Program. Lang., 2023 [PDF] [BIB] [external pagePublishercall_made][external pageextended versioncall_made]
- T. Dardinier, P. Müller, and A. J. Summers: Fractional Resources in Unbounded Separation Logic
Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), Proc. ACM Program. Lang., 2022. [PDF] [BIB] [external pagePublishercall_made]
- T. Dardinier, G. Parthasarathy, N. Weeks, P. Müller and A. J. Summers: Sound Automation of Magic Wands
Computer Aided Verification (CAV), 2022. [PDF] [BIB] [external pagePublishercall_made]
- G. Parthasarathy and P. Müller and A. J. Summers: Formally Validating a Practical Verification Condition Generator
Computer Aided Verification (CAV), 2021. [PDF] [BIB] [external pagePublishercall_made][external pageextended versioncall_made]
Completed Student Projects
- Hongyi Ling, Practical work
Formally Deriving an Equirecursive Viper Semantics via a Least Fixed Point Predicate Interpretation
- Lukas Himmelreich, Bachelor's thesis
DownloadFormally Validating the CFG Optimization Phase of the Boogie Program Verifier (PDF, 637 KB)vertical_align_bottom
- Ellen Arlt, Master's thesis
DownloadA Formally Verified Automatic Verifier for Concurrent Programs (PDF, 1.2 MB)vertical_align_bottom
- Aleksandar Hubanov, Bachelor's thesis
DownloadFormally Validating the AST-to-CFG Phase of the Boogie Program Verifier (PDF, 802 KB)vertical_align_bottom
- Nicola Widmer, Bachelor's thesis
Sound Automation of Magic Wands in a Symbolic-Execution Verifier
- Matthias Roshardt, Master's thesis
Extending the Viper Verification Language with User-Defined Permission Models
- Noé Weeks, Internship
Making Magic Wands Combinable
- Benjamin Bonneau, Internship
DownloadA Formal Foundation for the Dafny Verifier (PDF, 420 KB)vertical_align_bottom
- Thibault Dardinier, Master's Thesis
Beyond the Frame Rule: Static Inlining in Separation Logic
Acknowledgments
The project is being funded by the external pageSwiss National Science Foundationcall_made.