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 (please stick to this option!), where <pvsversion> identifies the PVS version used (preferrably "2.4")
<pvsversion>.<projlib>.<date>.<root_theory>.inclusive.dmp if the dump includes all other libraries (please DO NOT use this option!);

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" hyperlink in the project table below), before Wednesday 22 January 2010 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 27 January 2010 - 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 8 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 ?? January 2010 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! 27 January 2010
Graph library and graph coloring problem: continuation and improvement of last year related project.	CHARRE Martial EGRON Gerome GOURNAY Sylvain RICCIO Damien	main [pvs]	team1 [pvs, slides] prof advice	9:00am with Prof. ??? ???
Transitive closure of a finite relation: equivalence of a mathematical definition of transitive closure and a computational one, see last year related project: complete proofs, and redo from scratch, using a more general approach (based on operational and theoretical fixpoint)	El Assas Akram Martin Bousquet Arthur Redondy Pascal Noisette Théo Tatinclaux Cameron van den Bergh	main [pvs]	team2 [pvs] prof advice	9:30am with Prof. ??? ???
Marienbad game (a Nim variant): show that the second player has a winning strategy	TRAN QUANG Thanh Truc LONG Qin Qin Aïcha Hamza Laetitia Higonenq	main [pvs]	team3 [pvs] prof advice	10:00am with Prof. ??? ???
Adapt PVS 2.3 libraries of First Order Logic and Imperative Program Verification to PVS 2.4 (and/or higher).	Meryem Alaoui Soulimani Elizabeth Flores Chavez Ghileg Gharbi Saad Seffar	main [pvs]	team4 [pvs] prof advice	10:45am with Prof. ??? ???
Extend a library of matrix calculus developed over the years by previous students: generalize from real number to some adequate structure (probably a ring), and add some interesting theorems. [not sure what could be added ...];	Jendoubi Walid Boughanmi Hamdi Frikha Kamel Baccouche Taha	main [pvs]	team5 [pvs] prof advice	11:45am with Prof. ??? ???

Back to Top

Mini-project proposals

Team 1: Graph library and graph coloring problem: continuation and improvement of last year related project;
Team 2: Transitive closure of a finite relation: equivalence of a mathematical definition of transitive closure and a computational one, see last year related project: complete proofs, and redo from scratch, using a more general approach (based on operational and theoretical fixpoint);
Team 3: Marienbad game (a Nim variant): show that the second player has a winning strategy;
Team 4: Adapt PVS 2.3 libraries of First Order Logic and Imperative Program Verification to PVS 2.4 (and/or higher);
Team 5: Extend a library of matrix calculus developed over the years by previous students: generalize from real number to some adequate structure (probably a ring), and add some interesting theorems. [not sure what could be added ...];
Team ?: Limits of infinite sequences of real numbers: set up this new library, and prove a few classical theorems about limits.