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

Application domain/field

• Program verification
• Dynamic languages
• Deductive verification
• Concurrent programs

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