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