This webpage showcases several interesting examples that demonstrate features of Nagini, a static verifier for Python 3.

Binary Search Tree

Binary search tree implementation from interactivepython.org.

Cell and Recell

Demonstration of predicate families; running example of paper 'Separation Logic and Abstraction', POPL 2005.

Divisor

Method finding a divisor of an integer; demonstrates for loops and break statements.

Hello World (IO)

Program outputting the string 'Hello World', demonstrating input/output verification.

Quicksort

Quicksort implementation from rosettacode.com, demonstrating verification of termination.

Students

Different kinds of students enrolling in courses; demonstrating predicate families.

Sum of odd numbers

Calculates the sum of all odd integers in a list; demonstrates pure functions, built-in list types, and continue statements.

Tickets

Running example from CAV 2018 paper, showing dynamic field addition, quantifiers, predicates and termination verification.

Watchdog

Watchdog continually checks that other threads preserve an invariant on shared data; demonstrates verification of threads, locking, and deadlock freedom.

Empty Example (try your own!)

Input and verify a new example of your own