This webpage contains the full examples referenced in the paper "Viper: A Verification Infrastructure for Permission-Based Reasoning" published at VMCAI 2016. The experimental data used for the paper can be found by following this link.

Fig. 2: Sorted List

A sorted list of integers, implemented via immutable sequences, and a method that inserts an element into the list ...

Fig. 4: Guarded-by Monitor Invariant

A client of a sorted list that acquires a monitor (lock) before changing the list ...

Fig. 6: Linked-List (Predicates)

Inserting into an ordered linked-list which is specified via a recursively-defined predicate ...

Fig. 7: Linked-List (Magic Wands)

A variant of the 'Linked-List (Predicates)' example, in which the loop invariant uses a magic wand to bookkeep permissions ...

Fig. 8: 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 ...