Sur la preuve d’algorithmes, il faudrait regarder par exemple :
http://projects.laas.fr/IFSE/FMF/J3/slides/P004_Xavier_Leroy.pdf

Ce cours du LRI :
https://www.lri.fr/ paulin/B/poly001.html
ou cette page :
http://home.gna.org/brillant/2004-Moniot/B-mf.html

ou 2 sociétés sur la méthode B :
http://www.methode-b.com/preuve-formelle/
http://www.clearsy.com/actualites/le-26-juin-2013-a-paris-preuves-formelles-systeme-pour-le-cbtc-de-la-ligne-7-flushing-de-new-york/

Quand vous voyagez sur la ligne 14, et maintenant la ligne, vous utilisez du logiciel vérifié par la méthode B  http://fr.wikipedia.org/wiki/M%C3%A9thode_B