Vérification logicielle M2

Un panorama des méthodes formelles

Programmation certifiée en Coq


Exposés

Présentation de 13 minutes en binôme avec vidéoprojection du PDF réalisé (environ une douzaine de diapos).
- ANDRIANASOLO Tiavina et HOUMADI Farda, Viola: Trustworthy Sensor Notifications for Enhanced Privacy on Mobile Systems
- JAURES Arnold  et NATIVEL Christopher, Proving the Correctness of Heuristically Optimized Code
- BLANCA Mathieu et LOCATE Rechad, COGENT: Verifying High-Assurance File System Implementations
- EMIL Ben Djadid et RALANTOARIZAKA Nantenaina, Implementing TLS with Verified Cryptographic Security
- AKY Nathan et KOURBANHOUSSEN Idriss, Java Pathfinder
- CONSTRAINT Tony et TREMOULU Lorenzo, Java Modeling Language 
- CHANE Xavier et GAUVIN Cyril, Frama-C
- PAYET Bruno et PUAGNOL André, Finding and Understanding Bugs in C Compilers
- HOARAU Damien et TSANG Romain, Quark: A Web Browser with a Formally Verified Kernel
- ABDOU Kasimir et YOUSSOUFFOU Mohamed, Trace Based Verification of Imperative Programs with I/O
- PATEL Oumar, Spin
- AHAMADA Dalili et TSE-HAI-SHING Jean-François, Automating Formal Proofs for Reactive Systems
- ZAKARIASY Ketty, Extended Static Checking for Java

Exemple de thèmes


Evaluation


Annales


Ressources


Valid XHTML 1.0 Transitional