AutoProof Verified Code Repository

This code repository consists of algorithms and programs that have been successfully verified with AutoProof. You will find a description of each problem, a reference to where the problem was proposed (if applicable), as well as the source code of the solution. You can run the online version of AutoProof for each problem, or download the source code of the problems and run AutoProof on your machine (see the EVE website for installation instructions).

Name Description Source Category
(show all)
1

Arithmetic

Build arithmetic operations based on the increment operation.

VSI'08

Algorithm
2

Binary search

Binary search on a sorted array.

VSI'08

Algorithm
3

Board Game I

A simple board game application; players throw dice to move on a board.

Application
4

Board Game II

A more complex version of a board game with different square types.

Application
5

Closures

Various applications of function objects.

FAC'07

6

Command

Encapsulate complete information to execute a command (design pattern).

FAC'07

Design Pattern
7

Composite

A tree with a consistency constraint between parent and children nodes.

SAVCBS'08 / SC'14

Design Pattern
8

Doubly-Linked-List

Implementation of a linked list with links to left and right neighbours.

ECOOP'04 / SC'14

Data Structure
9

Dutch flag

Partition an array in three different regions (specific and general verions).

Algorithm
10

Hash-set

A hash set with mutable elements.

Data Structure
11

Iterator

Usage of multiple iterators over a mutable collection.

SAVCBS'06 / SC'14

Design Pattern
12

Linked queue

Queue implementation using a linked list.

VSI'08

Data Structure
13

Longest Common Prefix (LCP)

Longest common prefix starting at given positions x and y in an array.

FM'12

Algorithm
14

Map ADT

Generic map ADT with layered data.

VSI'08

Data Structure
15

Marriage

Consistency constraint between persons that can marry each other.

ECOOP'04

Invariant
16

Master clock

A number of slave clocks are loosly synchronized to a master.

MPC'04 / SC'14

Invariant
17

Observer

Multiple observers cache the content of a subject object (design pattern).

SAVCBS'07 / SC'14

Design Pattern
18

Priority-Inheritance-Protocol

A Compound with loosly connected nodes where cycles are possible.

IWACO'09 / SC'14

19

Ring buffer

A bounded queue implemented using a circular array.

VSTTE'12

Data Structure
20

Rotation

Circularily shift a list by k positions (multiple algorithms).

Furia'14

Algorithm
21

Search a list

Search a linked list for a given element.

VSTTE'10

Algorithm
22

Sorting

Sorting of integer arrays with quick sort, insertion sort, selection sort, bubble sort, and gnome sort.

Algorithm
23

Strategy

A program's behaviour is selected at runtime (design pattern).

FAC'07

Design Pattern
24

Sum and max

Calculate sum and maximum of an integer array simultaneously.

VSTTE'10

Algorithm
25

Tree Maximum

Find the maximum value in a binary tree.

COST'11

Algorithm
26

Two-way maximum

Find the maximum element in an array by searching from both ends.

COST'11

Algorithm
27

Two-way sort

Sort a boolean array in linear time using swaps at both ends.

VSTTE'12

Algorithm