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 | Doubly-linked list with re-insertion 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 |