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