see also the index (by topic, by tool, by reference, by year)
The VerifyThis Benchmarks
http://verifythis.cost-ic0701.org/
The VerifyThis benchmarks, a collection of verification benchmarks designed in the context of the COST Action IC0701 FoVeOOS: Formal Verification of Object-Oriented Software
- Amortized Queue, in Why3
- Binary search
- Binary search in C annotated in ACSL
- Filter elements of an array
- Inverting an Injection, in Why3
- Searching a Linked List, in Why3
- Selection Sort, Java version
- Sparse Arrays in Capucine
- Sparse Arrays in Why3
- Sum and Maximum, in Why3
- The N-queens problem, in Why3
see also the index (by topic, by tool, by reference, by year)