Galerie de programmes vérifiés
This is a new web page for Toccata gallery. It is still partly under reconstruction. You may find the former page at this URL
Cette page collecte des preuves de programmes effectuées dans notre équipe. Vous pouvez télécharger une archive de cette collection.
[Galerie générée le 07/03/2023. Nombre d'exemples : 240]
Par catégorie
- Algorithms [17 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 [20 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 [25 examples]
- Strings [5 examples]
- Trees [23 examples]
- Tricky termination [11 examples]
- Type invariant [2 examples]
- Words [4 examples]
Par référence
- 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]
Par outil
- 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 [203 examples]
Par date
- 2023 [1 example]
- 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)