PV4 Naginiverifies general properties like termination and deadlock freedom of Python programs

Application domain/field

Type of tool

Static verifier/deductive verifier

Expected input

Source code (statically-typed) with specifications (pre-/postconditions/loop invariants/etc.)

Format:

Python file

Expected output

Verified (i.e. specification holds) or an error

Internals

Automated verifier for statically-typed, concurrent Python 3 programs. The Python program is encoded into a Viper program. The program can then be verified using either symbolic execution or verification condition generation. "Nagini can verify memory safety, functional properties, termination, deadlock freedom, and input/output behavior." Uses Viper, mypy, Boogie
Concurrency Python

Links

Last commit date

18 May 2021

Related papers

Last publication date

18 July 2018

Related tools

Tools that also use Viper as a back end for verification: Gobra, Prusti and VerCors.

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.