This webpage showcases several interesting examples that demonstrate features of Nagini, a static verifier for Python 3.
Binary search tree implementation from interactivepython.org.
Demonstration of predicate families; running example of paper 'Separation Logic and Abstraction', POPL 2005.
Method finding a divisor of an integer; demonstrates for loops and break statements.
Program outputting the string 'Hello World', demonstrating input/output verification.
Quicksort implementation from rosettacode.com, demonstrating verification of termination.
Different kinds of students enrolling in courses; demonstrating predicate families.
Calculates the sum of all odd integers in a list; demonstrates pure functions, built-in list types, and continue statements.
Running example from CAV 2018 paper, showing dynamic field addition, quantifiers, predicates and termination verification.
Watchdog continually checks that other threads preserve an invariant on shared data; demonstrates verification of threads, locking, and deadlock freedom.
Input and verify a new example of your own