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  Build arithmetic operations based on the increment operation.  Algorithm  
2  Binary search on a sorted array.  Algorithm  
3  A simple board game application; players throw dice to move on a board.  Application  
4  A more complex version of a board game with different square types.  Application  
5  Various applications of function objects.  
6  Encapsulate complete information to execute a command (design pattern).  Design Pattern  
7  A tree with a consistency constraint between parent and children nodes.  Design Pattern  
8  Implementation of a linked list with links to left and right neighbours.  Data Structure  
9  Partition an array in three different regions (specific and general verions).  Algorithm  
10  A hash set with mutable elements.  Data Structure  
11  Usage of multiple iterators over a mutable collection.  Design Pattern  
12  Queue implementation using a linked list.  Data Structure  
13  Longest common prefix starting at given positions x and y in an array.  Algorithm  
14  Generic map ADT with layered data.  Data Structure  
15  Consistency constraint between persons that can marry each other.  Invariant  
16  A number of slave clocks are loosly synchronized to a master.  Invariant  
17  Multiple observers cache the content of a subject object (design pattern).  Design Pattern  
18  A Compound with loosly connected nodes where cycles are possible.  
19  A bounded queue implemented using a circular array.  Data Structure  
20  Circularily shift a list by k positions (multiple algorithms).  Algorithm  
21  Search a linked list for a given element.  Algorithm  
22  Sorting of integer arrays with quick sort, insertion sort, selection sort, bubble sort, and gnome sort.  Algorithm  
23  A program's behaviour is selected at runtime (design pattern).  Design Pattern  
24  Calculate sum and maximum of an integer array simultaneously.  Algorithm  
25  Find the maximum value in a binary tree.  Algorithm  
26  Find the maximum element in an array by searching from both ends.  Algorithm  
27  Sort a boolean array in linear time using swaps at both ends.  Algorithm 