Gallery of verified programs
This page collects program verifications performed in our team. You can download an archive of this collection.
[Gallery generated on 2025-03-14. Number of examples: 252]
By topic
- Algorithms [18 examples]
- Arithmetic [14 examples]
- Arithmetic Overflow [3 examples]
- Array Data Structure [79 examples]
- Bitwise operations [8 examples]
- Data Structures [35 examples]
- Divisibility [6 examples]
- Exceptions [3 examples]
- Floating-Point Computations [18 examples]
- Ghost code [34 examples]
- Graph Algorithms [10 examples]
- Historical examples [11 examples]
- Inductive predicates [13 examples]
- List Data Structure [15 examples]
- Mathematics [20 examples]
- Matrices [5 examples]
- Non-linear Arithmetic [11 examples]
- Permutation [10 examples]
- Pointer Programs [9 examples]
- Proofs by reflection [2 examples]
- Randomized Algorithms [2 examples]
- Searching Algorithms [5 examples]
- Semantics of languages [9 examples]
- Separation challenges [3 examples]
- Sorting Algorithms [25 examples]
- Strings [6 examples]
- Trees [25 examples]
- Tricky termination [11 examples]
- Type invariant [2 examples]
- Words [6 examples]
By reference
- CoLiS project [3 examples]
- Fourth Verified Software Competition (VSComp) 2014 [1 example]
- NSV-3 Benchmarks [5 examples]
- Project Euler [7 examples]
- ProofInUse joint laboratory [14 examples]
- The 1st Verified Software Competition [5 examples]
- The 2nd Verified Software Competition [5 examples]
- The Art of Computer Programming [3 examples]
- The COST FoVeOOS'11 Competition [11 examples]
- The VACID-0 Benchmarks [6 examples]
- The VerifyThis Benchmarks [11 examples]
- VerifyThis @ ETAPS 2015 [3 examples]
- VerifyThis @ ETAPS 2016 [2 examples]
- VerifyThis @ ETAPS 2017 [5 examples]
- VerifyThis @ ETAPS 2018 [7 examples]
- VerifyThis @ ETAPS 2019 [3 examples]
- VerifyThis @ ETAPS 2021 [5 examples]
- VerifyThis @ ETAPS 2024 [2 examples]
- VerifyThis @ FM2012 [3 examples]
By tool
- Alea [2 examples]
- Caduceus [1 example]
- Capucine [1 example]
- Coq [16 examples]
- Frama-C [21 examples]
- Gappa [9 examples]
- J3 [1 example]
- Jessie [20 examples]
- Krakatoa [11 examples]
- SPARK 2014 [9 examples]
- Why3 [212 examples]
By year
- 2025 [1 example]
- 2024 [8 examples]
- 2023 [4 examples]
- 2022 [1 example]
- 2021 [10 examples]
- 2020 [7 examples]
- 2019 [14 examples]
- 2018 [17 examples]
- 2017 [12 examples]
- 2016 [21 examples]
- 2015 [17 examples]
- 2014 [24 examples]
- 2013 [11 examples]
- 2012 [29 examples]
- 2011 [44 examples]
- 2010 [20 examples]
- 2009 [2 examples]
- 2008 [3 examples]
- 2007 [7 examples]
see also the index (by topic, by tool, by reference, by year)