see also the index (by topic, by tool, by reference, by year)
Why3
A platform for deductive program verification.
- A Certified First-Order Theorem Prover
- A Formal Proof of a Unix Path Resolution Algorithm
- A Formally Verified Interpreter for the Shell-like Language CoLiS
- A Formally Verified Symbolic Interpreter for a IMP language
- A Sudoku solver
- A challenge related to the Esterel Compiler
- A simple example of amortization
- A small mathematical puzzle from a Dijkstra paper
- A small puzzle involving a Roberval balance
- A tiny register allocator for tree expressions
- A toy variant of Fibonacci function
- AVL trees
- Algorithm 63 (partition)
- Algorithm 64 (quicksort)
- Algorithm 65 (find)
- Amortized Queue, in Why3
- An Efficient Arbitrary-Precision Integer Library
- An example from EWD 673
- Approximated Cosine in Why3
- Area of a triangle
- Base64
- Bellman-Ford algorithm
- Binary Heaps in Why3
- Binary Sort
- Binary Square Root
- Binary multiplication
- Binary search
- Binomial coefficients
- Binomial heaps
- Boyer and Moore's MJRTY algorithm (1980)
- Braun Trees
- Bresenham line drawing algorithm
- Bubble sort
- Build a balanced tree from a list
- Call-by-value reduction of SK terms
- Check an array of integers for duplicate values
- Checking that a word is a Dyck word
- Circular queue in an array
- Coincidence count
- Coincidence count, using lists
- Common factor of two words
- Computing the height of a tree in CPS style
- Computing the number of solutions to the N-queens puzzle
- Conjugate of a partition
- Counting bits in a bit vector
- Cursor examples
- Depth-First Search
- Dijkstra's national flag
- Dijkstra's national flag (variant)
- Dijkstra's shortest path algorithm
- Disambiguation of Plus Expressions
- Double WP
- Edition distance
- Equality up to spaces
- Euclidean division
- Euler's Sieve
- Exact subtraction: Sterbenz's theorem
- Extract non-zero values from an array
- Fast exponentiation
- Fenwick
- Fibonacci function, linear/logarithmic algorithms, Why3 version
- Fibonacci with memoization
- Find a value in a sorted list of integers
- Find the maximal element in an array
- Find the shortest path in a directed graph using BFS
- FoVeOOS'11 Competition: challenge 1, in C
- FoVeOOS'11 Competition: challenge 1, in Java
- FoVeOOS'11 Competition: challenge 1, in Why3
- FoVeOOS'11 Competition: challenge 2 in Why3
- FoVeOOS'11 Competition: challenge 2, in C
- FoVeOOS'11 Competition: challenge 2, in Java
- FoVeOOS'11 Competition: challenge 3 in Why3
- FoVeOOS'11 Competition: challenge 3, in C
- FoVeOOS'11 Competition: challenge 3, in Java
- Generate all binary trees of size n
- Gnome Sort
- Greatest common divisor with Bezout coefficients
- Greatest common divisor, using the Euclidean algorithm
- Hash table implementation
- Hash tables with linear probing
- Hexadecimal encoding of strings
- Hillel challenge
- Hoare Logic and Games
- Hoare's Proof of a Program: FIND
- Huffman with two queues
- I can't believe it can sort
- In-Place Linked-List Reversal in Why3
- Infinity of primes
- Insertion sort (arrays)
- Insertion sort (lists)
- Integer cubic root
- Integer square root
- Integer square root on machine integers
- Inverse in place
- Inverting an Injection, in Why3
- Kleene Algebra
- Knuth's prime numbers
- Knuth-Morris-Pratt string searching algorithm
- Koda-Ruskey's algorithm
- Largest prime factor
- Leftist heaps
- Maximal sum in a matrix
- Maximize product of adjacent numbers in a matrix
- Maximum subarray problem
- Maze building from the VACID-0 benchmarks
- McCarthy's 91 function
- Mergesort (arrays)
- Mergesort (lists)
- Mergesort (queues)
- Minimum and maximum of an array of integers
- Minimum excludant (aka mex)
- Most Frequent Value in a Sorted Array
- Mutual recursion
- Optimal replay
- Pairing heaps
- Pairing heaps (variant)
- Pancake sorting
- Pigeonhole principle
- Program proofs from Floyd's Assigning Meanings to Programs (1967)
- Program verification examples from the book "Software Foundations"
- Proof from Turing's Checking a Large Routine (1949)
- Queue implemented using two lists
- Quicksort (arrays)
- Random Access Lists
- Red-black trees
- Regular expression matching using residuals
- Remove duplicate elements in an array, in-place
- Removing an element from a singly-linked list
- Removing duplicate elements in an array, using a mutable set
- Resizable arrays
- Ring Buffer
- Ropes
- Same fringe
- Schorr-Waite algorithm
- Schorr-Waite algorithm, proof using a ghost monitor
- Schorr-Waite algorithm, proof via recursion
- Searching a Linked List, in Why3
- Searching a zero in an array where values never decrease by more than one
- Selection sort (arrays)
- Sieve of Eratosthenes
- Skew heaps
- Snapshotable Trees
- Sort an array of Boolean values
- Sort an array of integers, assuming all elements are in the range 0..k-1
- Sparse Arrays in Why3
- String search
- Subsequence
- Sum and Maximum, in Why3
- Sum of even-valued Fibonacci numbers
- Sum of multiples of 3 and 5
- Sum queries
- Summing the elements of a list
- Tarski fixed point theorem
- The BitWalker, Why3 version
- The N-queens problem, in Why3
- The N-queens problem, using bit vectors
- The rightmost bit trick
- Three idempotent rings
- Topological sorting
- Tortoise and hare algorithm
- Towers of Hanoi
- Toy compiler
- Traversing a tree inorder, filling an array
- Tree of array
- Tree reconstruction from a list of leave depths
- Tree relabelling
- Two puzzles from Danvy and Goldberg's ``There and back again''
- Unraveling a Card Trick
- VSCOMP 2014, problem 1
- Variations on Semantics of Programming Languages
- Various programs computing the factorial, in Why3
- Various ways of proving an induction principle
- VerifyThis 2015: solution to problem 1
- VerifyThis 2015: solution to problem 2
- VerifyThis 2015: solution to problem 3
- VerifyThis 2016: Binary Tree Traversal
- VerifyThis 2016: Strassen's Matrix Multiplication
- VerifyThis 2017: Maximum-sum submatrix
- VerifyThis 2017: Odd-even transposition sort
- VerifyThis 2017: Odd-even transposition sort (alt)
- VerifyThis 2017: Pair Insertion Sort
- VerifyThis 2017: Tree Buffer
- VerifyThis 2018: Array-based queuing lock
- VerifyThis 2018: Array-based queuing lock (alt)
- VerifyThis 2018: Register allocation
- VerifyThis 2018: le rouge et le noir
- VerifyThis 2018: le rouge et le noir (alt)
- VerifyThis 2018: mind the gap
- VerifyThis 2018: mind the gap (alt)
- VerifyThis 2019: Cartesian trees
- VerifyThis 2019: GHC sort
- VerifyThis 2021: DLL to BST
- VerifyThis 2021: Lexicographic Permutations (version 1)
- VerifyThis 2021: Lexicographic Permutations (version 2)
- VerifyThis 2021: Shearsort
- VerifyThis 2021: Shearsort (modified)
- VerifyThis @ FM 2012, problem 1
- VerifyThis @ FM 2012, problem 2
- VerifyThis @ FM 2012, problem 3
- WP revisited in Why3
- Warshall algorithm
- White and black balls
- Wrap lines
see also the index (by topic, by tool, by reference, by year)