Nagini
Nagini is an automated, modular verifier for (concurrent) Python programs, based on the Viper verification infrastructure. It supports a rich subset of statically-typed Python 3 as defined in external pagePEP 484. Nagini is intended to be able to prove complex properties of real-world user code; in addition to basic safety and functional correctness, its specification language allows specifying properties like input/output behavior, progress properties, and secure information flow.
Nagini was originally developed as part of the VerifiedSCION project; it is open source and available on external pageGithub.
Nagini has also served as the basis of 2vyper, a verifier for Ethereum smart contracts written in the Python-like Vyper language.
Project Members
Publications
- M. Eilers and S. Meier and P. Müller, Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security
In Computer Aided Verification (CAV), 2021. [PDF]
- M. Eilers and P. Müller, Nagini: A Static Verifier for Python
In Computer Aided Verification (CAV), 2018. [DownloadPDF]
- M. Hassan and C. Urban and M. Eilers and P. Müller, MaxSMT-based Type Inference for Python 3
In Computer Aided Verification (CAV), 2018. [DownloadPDF]
Completed Student Projects
- Severin Meier, Master's Thesis
Verification of Information Flow Security for Python Programs - Benjamin Schmid, Bachelor's Thesis
Abstract Read Permission Support for an Automatic Python Verifier - Benjamin Weber, Master's Thesis
Automatic Verification of Closures and Lambda-Functions in Python - Mostafa Hassan, Bachelor's Thesis
Static Type Inference for Python
- Vytautas Astrauskas, Master's Thesis
Input/Output Verification in Viper