examples

PVS‎ > ‎

We have implemented several PVS libraries over the years, at LaBRI and ENSEIRB-MATMECA: some of them are general purpose; others are more like illustrative examples PVS specification and proof. Students have also contributed, on academic projects. One of the difficulty is to maintain compatibility with new PVS releases. We are presenting some examples here, with the aim of gradually offering more!

“Le compte est bon” (count_ok_all), one of 2006-2007 ENSEIRB student projects: correctness and completeness of an algorithm computing a list of all solutions to a given problem, derived from an earlier algorithm (and PVS) library (count_ok), computing a first solution to the problem, when there is one, see

2.4.count_ok_all.16jan2007at22h41.count_ok_all.dmp.txt (compatible with PVS 5.0, but the main proof is broken);
requiring 2.4.count_ok.12mar2002.dump.dmp.txt (compatible with PVS 5.0, all proofs still complete);

Correctness of a compiler of algebraic expressions;
Dutch flag;
First order logic and imperative programming;
Graph coloring: N+1 colors are enough to color a finite graph of degree N (student project);
Multisets and permutations on a monoid;
Well founded relations.

More examples in the world of PVS users

NASA Langley formal methods: include many PVS libraries, some of which are now part of PVS standard library;
University of Seville.

These are referenced by PVS wiki (which is not very active), but there are (or have been) a lot more users, who have developed substantial libraries in various domains.

Sous-pages (3) : compiler Graph coloring project Well founded relations

Comments

edu	Rechercher dans ce site