This webpage showcases several interesting examples that demonstrate features of the Viper verification infrastructure
Binary Search (Quantified Permissions)
Binary search in a sorted (mutable) array
Binary Search (Seq)
Binary search in a sorted (mathematical) sequence
Dutch Flag (Quantified Permissions)
Dutch Flag algorithm for coarse sorting of an array
Graph Copy (Quantified Permissions)
Duplicating a heap-allocated (mutable) graph
Graph Marking (Quantified Permissions)
A graph marking algorithm (in the spirit of mark-and-sweep garbage collectors) ...
Array Max, by elimination (Quantified Permissions)
Finding the maximum in an array by elimination (COST IC0701 Verification Competition 2011)
Array Max, straight-forward (Quantified Permissions)
Finding the maximum in an array the straight-forward way
Quickselect (Quantified Permissions)
An encoding of the Quickselect algorithm over arrays
Iterative Tree Delete (Magic Wands)
Deletion of minimal tree element (VerifyThis@FM2012)
Parallel Array Replace (Quantified Permissions)
Running example from the CAV'16 paper: replace each occurrence of an element in an array segment by recursing over the two half-segments in parallel ...
Longest Common Prefix (Quantified Permissions)
Challenge from the VerifyThis Verification Competition 2012: finding the longest common prefix in an array ...
Sorted List
A sorted list of integers, implemented via immutable sequences, and a method that inserts an element into the list ...
Guarded-by Monitor Invariant
A client of a sorted list that acquires a monitor (lock) before changing the list ...
Linked-List (Predicates)
Inserting into an ordered linked-list which is specified via a recursively-defined predicate ...
List Iterator (Magic Wands)
An iterator protocol, for iterating over a linked list ...
Array-List (Quantified Permissions)
Inserting into an array-list which is specified via quantified permissions (iterating separating conjunction) ...
Encoding ADTs
An encoding of a Haskell-style Nil-Cons-list, alongside proofs of certain properties of the encoded abstract data type, and a pattern match exhaustiveness check ...
Empty Example (try your own!)
Input and verify a new example of your own