[Why3-club] gallery of verified programs

Jean-Christophe Filliâtre Jean-Christophe.Filliatre at lri.fr
Thu Nov 1 11:20:11 CET 2012


Dear users,

Our gallery of programs verified with Why3 has been updated to version 0.80:

   http://proval.lri.fr/gallery/why3.en.html

Some examples have been improved using type invariants and ghost code, e.g.

   http://proval.lri.fr/gallery/vacid_0_sparse_array.en.html
   http://proval.lri.fr/gallery/vstte12_ring_buffer.en.html
   http://proval.lri.fr/gallery/vstte10_aqueue.en.html

New examples are:

   http://proval.lri.fr/gallery/algo63.en.html
   http://proval.lri.fr/gallery/algo64.en.html
   http://proval.lri.fr/gallery/algo65.en.html
   http://proval.lri.fr/gallery/binary_sqrt.en.html
   http://proval.lri.fr/gallery/optimal_replay.en.html
   http://proval.lri.fr/gallery/resizable_array.en.html
   http://proval.lri.fr/gallery/verifythis_PrefixSumRec.en.html
   http://proval.lri.fr/gallery/add_list.en.html

Enjoy,
-- 
Jean-Christophe



More information about the Why3-club mailing list