see also the index (by topic, by tool, by reference, by year)
Data Structures
Examples of verified data structures
- AVL trees
- Amortized Queue, in Why3
- Binary Heaps in Why3
- Binomial heaps
- Braun Trees
- Build a balanced tree from a list
- Cartesian Trees (from VerifyThis 2019) in SPARK
- Circular queue in an array
- Cursor examples
- Fenwick
- Flexible Arrays
- Hash table implementation
- Hash tables with linear probing
- Just Join
- Leftist heaps
- Pairing heaps
- Pairing heaps (variant)
- Queue implemented using two lists
- Queues, in SPARK
- Random Access Lists
- Red-Black Trees in SPARK
- Red-black trees
- Resizable arrays
- Ring Buffer
- Ropes
- Skew heaps
- Sparse Arrays in Capucine
- Sparse Arrays in Why3
- VerifyThis 2015: solution to problem 1
- VerifyThis 2015: solution to problem 3
- VerifyThis 2017: Tree Buffer
- VerifyThis 2018: mind the gap
- VerifyThis 2018: mind the gap (alt)
- VerifyThis 2019: Cartesian trees
see also the index (by topic, by tool, by reference, by year)