see also the index (by topic, by tool, by reference, by year)
2016
Examples of year 2016
- A Formal Proof of a Unix Path Resolution Algorithm
- A challenge related to the Esterel Compiler
- A tiny register allocator for tree expressions
- Abstract models and refinement in SPARK: allocators example
- Binary multiplication
- Binomial heaps
- Depth-First Search
- Euler Project problem 11, SPARK/Ada version
- Integer cubic root
- Koda-Ruskey's algorithm
- Leftist heaps
- Maximize product of adjacent numbers in a matrix
- Pairing heaps
- Pairing heaps (variant)
- Schorr-Waite algorithm, proof via recursion
- The BitWalker, SPARK version
- The BitWalker, Why3 version
- VSCOMP 2014, problem 1
- VerifyThis 2016: Binary Tree Traversal
- VerifyThis 2016: Strassen's Matrix Multiplication
- White and black balls
see also the index (by topic, by tool, by reference, by year)