Ce projet a été effectué en quatrième année du CMI Informatique à l'UFR SFA Université de Poitiers dans le cadre de l'enseignement Logiciels sûrs.
Ce projet a été développé en trinôme avec l'IDE Visual Studio Code.
Notre code se trouve dans le fichier projet.ml, ce fichier peut être interprété pas à pas ou bien être exécuté.
Pour exécuter notre projet, il suffit d'utiliser la commande make qui compile les sources, vous pouvez ensuite lancer le projet avec la commande ./a.out.
- Vérification formelle de logiciels
- Introduction à l’assistant de preuves Coq
- Validation et vérification d’un programme
- Preuve de propriétés d’un programme
- Limites des techniques de tests
- Vérification par la preuve formelle de programmes
- Périmètre de la vérification formelle
- Notions d’équivalence de programmes et de transformations de programmes
- Logique de Hoare
- Triplets de Hoare
- Assertions
- Décoration de programmes
- Invariants de boucles
- Précondition la plus faible
Nous avons obtenu la note de 20/20.
This project was done in the fourth year of the CMI Computer Science at the UFR SFA Université de Poitiers in the context of the teaching Secure software.
This project was developed in trinomial with the IDE Visual Studio Code.
Our code is in the file project.ml, this file can be interpreted step by step or executed.
To execute our project, you just have to use the command make which compiles the sources, you can then launch the project with the command ./a.out.
- Formal software verification
- Introduction to the Coq proof assistant
- Validation and verification of a program
- Proof of program properties
- Limits of testing techniques
- Verification by formal proof of programs
- Perimeter of formal verification
- Notions of program equivalence and program transformations
- Hoare logic
- Hoare's triplets
- Assertions
- Decoration of programs
- Loop invariants
- Weakest precondition
We obtained a score of 20/20.