Home > Research > Students/Post-docs > Romain Salles

Romain Salles

Model-checking de programmes Java

Saturday 1 January 2011

Years: 2009 (IRL Ensimag)
Co-supervisor: David Monniaux
Subject: Model-checking de programmes Java
Abstract:

Ce sujet était au départ inspiré du sujet de Loïc Crétin l’année précédente. Vu les difficultés que posaient l’intégration des briques de base, nous avons décidé de nous passer d’un certain nombre d’entre elles : pas de front-end de compilateur complexe, pas de bibliothèque externe. Cette-fois, nous travaillons avec le byte-code Java, et la seule bibliothèque est ASM, qui permet de lire simplement ce byte-code. L’idée est de générer du code pour le model-checker NuSMV, et de l’utiliser pour prouver des propriétés sur des programmes booléens.

La traduction a été entièrement implémentée, et testée sur des exemples tirés d’un cours de programmation concurrente : différentes variantes de l’algorithme de Dekker (une correcte, et d’autres avec problèmes de synchronisation comme famine, dead-lock, propriété d’exclusion mutuelle violée, ...). L’outil a prouvé la version correcte et trouvé les contre-exemples pour les autres.


View online : Résumé sur Ensiwiki

Attached documents


Valid XHTML 1.0 Transitional
SPIP | | Site Map | Follow site activity RSS 2.0
Graphic design (c) styleshout under License Creative Commons Attribution 2.5 License