Gallery of verified programs
This is a new web page for Toccata gallery. It is still partly under reconstruction. You may find the former page at this URL
This page collects program verifications performed in our team. You can download an archive of this collection.
[Gallery generated on 2022-05-24. Number of examples: 238]
By topic
- Algorithms [16 examples]
- Arithmetic [14 examples]
- Arithmetic Overflow [3 examples]
- Array Data Structure [76 examples]
- Bitwise operations [8 examples]
- Data Structures [32 examples]
- Divisibility [6 examples]
- Exceptions [3 examples]
- Floating-Point Computations [16 examples]
- Ghost code [33 examples]
- Graph Algorithms [10 examples]
- Historical examples [8 examples]
- Inductive predicates [13 examples]
- List Data Structure [13 examples]
- Mathematics [19 examples]
- Matrices [5 examples]
- Non-linear Arithmetic [10 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 [24 examples]
- Strings [4 examples]
- Trees [23 examples]
- Tricky termination [11 examples]
- Type invariant [2 examples]
- Words [4 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 @ FM2012 [3 examples]
By tool
- Alea [2 examples]
- Caduceus [1 example]
- Capucine [1 example]
- Coq [16 examples]
- Frama-C [21 examples]
- Gappa [9 examples]
- Jessie [20 examples]
- Krakatoa [11 examples]
- SPARK 2014 [9 examples]
- Why3 [201 examples]
By year
- 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)