CVFP Conception et vérification formelle de programmes 
Software design and verification - Projects

Magistère informatique et télécommunications - ENS Rennes - Année 2013/2014

Monday 9 december, 2pm --> 4pm, room I60 (ISTIC)
Objectives:
- present a problem in software design / verification
- present a solution
- present a demo of an existing software (prover, model checker, tool) to solve the problem

During 2 hours, you will welcome people and present your work. You should prepare:
- some "posters" in A4 format (maybe one for the wall and some on the table)
- a good example for the demo

Evaluation
- quality of the "posters"
- quality and relevance of the example and the demonstration
- clarity of the explanation
- quality of the global work





1) Consistency of UML class diagrams
The project is based on the paper:

Reasoning on UML class diagrams
Daniela Berardi, Diego Calvanese, Giuseppe De Giacomo
Artificial Intelligence Journal, 2005

Study the embedding of UML class diagram in description logic
Use an automatic description logic solver such as Fact++. Here is a list of solvers:
Fact a prover for description logic
Fact++, the same prover in C++
A comprehensive list of provers for description logic
You may compare this approach with http://alloy.mit.edu/alloy/



2) Discovery of the aspect-oriented programming
You may base your presentation on:

Kiczales, G., Lamping, J., Mendhekar, A., Maeda, C., Lopes, C., Loingtier, J. M., & Irwin, J. (1997). Aspect-oriented programming (pp. 220-242). Springer Berlin Heidelberg.

- Present the aspect-oriented programming
- Show a demo with http://eclipse.org/aspectj/
- The demo may explain how to add a functionnality to your software. The functionnality to do should be tricky to add when we do not use aspect-oriented programming.
- Do not forget to make your demo easy to reinitialize: the demo should be reproducible many times.




3) Symbolic model checking in CTL
You may read the chapter about symbolic model checking in

Baier, C., & Katoen, J. P. (2008). Principles of model checking (Vol. 26202649). Cambridge: MIT press.


- Present symbolic model checking
- BDD
- Show a demo with nuSMV
- You may read the chapter about symbolic model checking in Principles of model checking
- The "poster" may show how the Kripke structure of your model is represented symbolically.




4) Modern model checking: from the code to a Kripke structure
- This project may be either abstraction and/or bounded model checking.
- Show a demo with any other tools that starts from a program written in a "real" language, for instance:
- http://spinroot.com/modex/ that abstracts a C program into a Spin model written in Promela
- BLAST that abstract a C program into a model
- http://bandera.projects.cis.ksu.edu/ that abstracts a  Java program into Spin or SMV models
- see also http://en.wikipedia.org/wiki/List_of_model_checking_tools
The "poster" may show the program you start with. You may show also the Kripke structure (or an idea of it) that is used by the model checking procedure.
Java Path Finder (not sure it makes abstraction)



5) Interesting tactics in Coq
    → Choisir une ou plusieurs tactiques automatisées de Coq (lia, lra, fourier, omega, ring, congruence, tauto, …).  Pas forcément la peine d’en prendre plusieurs :  une présentation complète d’une tactique sera probablement meilleur qu’une présentation partielle de plusieurs d’entre elles.
    → Présenter la ou les tactiques choisies :  quels types de problème résolvent-elles ?  Quelles sont les libertés sur l’énoncé que l’on peut prendre ?  Y a-t-il moyen de réduire plus ou moins simplement des classes un petit peu plus grandes vers un problème résoluble par cette ou ces tactiques ?
    → Présenter leur fonctionnement interne :  quel est l’algorithme utilisé ?  Éventuellement des études de complexités ou des discussions par rapport à la forme et la taille des termes de preuve fournis.
    → Une démo (de préférence partant d’un problème n’étant pas immédiatement résolu par la tactique et montrant comment le transformer pour que ça marche… mais on peut aussi tenter de comparer ce que la même preuve donnerait sans utiliser la tactique magique).
    → Ceci ne sont que des pistes parmi d’autres.



This project will not be presented:

dead) OCL (or JML)
The project consists in studying tools for OCL (the first order language in UML), JML (a first order language for specify JAVA programs) or variant. Eg.:
http://gres.uoc.edu/UMLtoCSP/
http://eclipseclp.org/
http://alloy.mit.edu/alloy/