see also the index (by topic, by tool, by reference, by year)
Martin Clochard
- A Certified First-Order Theorem Prover
- A Formal Proof of a Unix Path Resolution Algorithm
- A tiny register allocator for tree expressions
- AVL trees
- Check an array of integers for duplicate values
- Checking that a word is a Dyck word
- Double WP
- Fenwick
- Hash tables with linear probing
- Hoare Logic and Games
- Inverse in place
- Largest prime factor
- Remove duplicate elements in an array, in-place
- Schorr-Waite algorithm, proof using a ghost monitor
- Schorr-Waite algorithm, proof via recursion
- Sieve of Eratosthenes
- Tarski fixed point theorem
- Variations on Semantics of Programming Languages
- VerifyThis 2015: solution to problem 2
- VerifyThis 2016: Binary Tree Traversal
- VerifyThis 2016: Strassen's Matrix Multiplication
- VerifyThis 2018: Array-based queuing lock
- VerifyThis 2018: le rouge et le noir (alt)
- VerifyThis 2018: mind the gap
- VerifyThis 2021: Shearsort
- Warshall algorithm
see also the index (by topic, by tool, by reference, by year)