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.
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  Nondeterministic implementation of the Euclid's algorithm with termination guarantees  Algorithm  
9  Doublylinked list with reinsertion operation  Data Structure  
10  Implementation of a linked list with links to left and right neighbours.  Data Structure  
11  Partition an array in three different regions (specific and general verions).  Algorithm  
12  A hash set with mutable elements.  Data Structure  
13  Usage of multiple iterators over a mutable collection.  Design Pattern  
14  Queue implementation using a linked list.  Data Structure  
15  Longest common prefix starting at given positions x and y in an array.  Algorithm  
16  Generic map ADT with layered data.  Data Structure  
17  Consistency constraint between persons that can marry each other.  Invariant  
18  A number of slave clocks are loosly synchronized to a master.  Invariant  
19  Multiple observers cache the content of a subject object (design pattern).  Design Pattern  
20  A Compound with loosly connected nodes where cycles are possible.  
21  Determine if a sequence is a relaxed prefix of another sequence  Algorithm  
22  A bounded queue implemented using a circular array.  Data Structure  
23  Circularily shift a list by k positions (multiple algorithms).  Algorithm  
24  Search a linked list for a given element.  Algorithm  
25  Sorting of integer arrays with quick sort, insertion sort, selection sort, bubble sort, and gnome sort.  Algorithm  
26  A program's behaviour is selected at runtime (design pattern).  Design Pattern  
27  Calculate sum and maximum of an integer array simultaneously.  Algorithm  
28  Find the maximum value in a binary tree.  Algorithm  
29  Find the maximum element in an array by searching from both ends.  Algorithm  
30  Sort a boolean array in linear time using swaps at both ends.  Algorithm 