Mini-Project description

Students propose their own project as early as possible: a formalization of some topics and corresponding proofs to be done under PVS. Each project is done by a team of four students. Look at previous year projects to make sure your project is a new one. Note: you may choose an existing project provided you will add some value. For instance, if the proofs were not complete, and your proofs are, this is "added value".

You may also choose your project from the list of mini-project proposals: first come, first served!

Mini-project deliverable

Let "username" be the username of one of the team members at ENSEIRB.

Each project will be stored into ~username/public_html/pvs_project/ directory that will contain, at least, the following data:

index.html, an "html" index to all information related to the project, including:

the names of the authors of the project,
a clear statement of the subject of the project,
a conceptual analysis, with mathematical ideas of the proof(s), and their mapping into the PVS realization, rather than a "copy" of PVS proofs,
the status of your PVS implementation: are all proofs complete?
what are the author own contributions, what libraries belong to whom: for each PVS library which does not belong to you, clearly refer to the original dump (with its exact name and location in your PVS directory, see below) and indicate the URL of the page from which you downloaded this dump;
how to reconstruct the PVS project libraries from the dump(s) provided, and what version of PVS was used (normally PVS 2.4); [You should test your reconstruction procedure on some test directory.]

pvs, a directory containing:

<projlib>, the main project library, will contain at least

a dump of the root theory in this library under the form

<pvsversion>.<projlib>.<date>.<root_theory>.dmp if it does not include other libraries, where <pvsversion> identifies the PVS version used (preferrably "2.4")
<pvsversion>.<projlib>.<date>.<root_theory>.inclusive.dmp if the dump includes all other libraries;

a <lib> directory for each needed library, where <lib> clearly indicates the source of the library, e.g.,

nasa/fixpoints for Bruno Dutertre library copied from NASA,
enseirb/wf for my well founded relation library available at ENSEIRB,
team4/permutations for a library on permutations currently developped by another team,
my_lib for a personal library,

and the <lib> directory contains at least a dump of the corresponding library (which normally does not include other libraries, except if the dump comes from elsewhere, and did originally contain sub-libraries).

[Do not include PVS standard libraries (prelude, or libraries available from PVS installation directory "/opt/pvs/2.4/lib/" or "/opt/pvs/3.2/lib/": these libraries should not be copied into your pvs directory; theories you need should be directly imported, without using a "LIBRARY" declaration, e.g.,

"IMPORTING finite_sets@finite_sets_sums[nat]".]

Make sure that your project directory is translatable (use relative links in html files, except for URLs referring to the outside world, such as NASA, and relative pathes in PVS LIBRARY statements). Make sure that I have read access! I will use the "tar" command to copy your project directory into my own directory. Your project directory will be made available from the table below, using the team name, e.g., team5, as name.

Remark: the "index.html" top level file may be replaced with "index.htm" or "index.php", as it will not be included in the URL of your project in the table below: check the links in front of your project.

Mini-project initial announcement

Initial mail (any time, the sooner the better): please send me and/or IT304-IT305 La Forge forum "6 teams of 4 students each" thread an initial mail, with copy to all team members, including

the title of the chosen project;
the name of your team (team1 | ... | team6), see Student mini-projects;
the username of the team member responsible for hosting the project in his ~username/public_html/pvs_project/ directory;
the complete ENSEIRB URL of your project, that is, "http://www.enseirb.fr/~username/pvs_project/".

This will allow closer interaction between you and me, in the course of your project.

Mini-project final notification

Final mail: Please send me a mail with copy to all authors, telling me the address of the project directory (which should be the same as the one specified in your initial mail, and correspond to the one specified by the "main" hyperling in the project table below), before Wednesday 21 January 2009 at 11:59pm (23h59 french time). Do not change anything after sending the mail!

If you need help, please do not wait until the last minute! Come to me with the most recent PVS dump, use La Forge forum ... Note that I will be difficult to reach after around Thursday 15 January 2009!

Remark: there will be a project defence in the context of IT304 twin module.

Mini-project defence 22 January 2009 - all morning from 9:00am to 12:15pm - room I107

Students will defend their project in English, according to the planning below:

30 minutes per team, including 10 minutes of questions,
videoprojector and my Sony Vaio (with 3 button optical mouse) available under Windows Vista + White Board and Pens

tanit session available through Putty / Xming, although you are strongly advised NOT TO do a demo!
Google Chrome Beta, Mozilla Firefox 2.0, Internet Explorer 7 and Microsoft Power Point 2007 available under Windows.

[Please include all material used for the defence in your project directory, and reference it from your project page.]

A preparatory session will be organized on 16 January 2009 by your professors of English, see planning prepared by Ms Céline Guillon from CReL for details.

Student mini-projects

Note: Hours of defence are subject to changes!;[We may try to stick with Team ordering, which is currently the case.]

Subject	Team	Student project URL	Project archive prof advice	Public Defence All students must attend whole session! Thursday 22 January 2008
Permutations	Khaoula BEN ABDA Stéphanie GATTI Mohamed MAKHLOUF Florian THIBERVILLE	main [pvs]	team1 prof advice	9:00am with Prof. Paul Crocker
Transitive closure of a finite relation	BOUSQUET Rémi DUPREY Stéfanie DURAND Brice MAZEREAU Christelle	main [pvs]	team2 prof advice	9:30am with Prof. Paul Crocker
Sum on a list equivalent to sigma on a set	BERTHOME Valentin HENRY Nicolas KAIDI Sanna CATANESE Cécilia	main [pvs]	team3 prof advice	10:00am with Prof. Paul Crocker
Blue White Red flag	FAGOAGA Fabien GARCIA Alice JOUBERT Matthieu COHE Aurelie	main [pvs]	team4 prof advice	10:45am with Prof. Paul Crocker
Graph library and coloring problem	Fromi Romain Gondet Romain Ratouit Thomas Gentillet Christophe	main [pvs]	team5 prof advice	11:15am with Prof. Paul Crocker
Powerset	Armarolli Christophe Bieri Arnaud Juhoor Idriss Lavaure Fabrice	main [pvs]	team6 prof advice	11:45am with Prof. Paul Crocker

Back to Top

Mini-project proposals

Graph library and graph coloring problem: continuation and improvement of two last year related projects;
Permutations: continuation and improvement of last year projects about permutations, mainly about equivalence of multiset based definition with a an inductive definition;
Blue-white-red flag: continuation and improvement of last year project (mainly prove that output array is a permutation of input one);
Transitive closure of a finite relation: equivalence of a mathematical definition of transitive closure and a computational one;
The sum on a list is equal to some Sigma on a finite set;
Set of subsets (powerset): equivalence between a mathematical definition of the set of subsets of a finite set, and a computational one (using lists to represent sets); prove that the cardinality of the powerset is 2^N, for a set of cardinality N.