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