Résumé de séminaire

Résumé :

L'exposé présente l'expérience menée au sein de l'équipe Everest de l'INRIA sur la validation formelle d'applets Java pour carte à puces. Il décrit un outil qui permet de prouver formellement des classes Java annotées avec JML. JML est un langage d'annotation pour Java qui permet de décrire des invariants de classe et des comportements de méthodes. Je présenterai les bases (principalement un calcul de plus faible précondition sur des sources annotées de Java) et les caractéristiques principales de l'outil. La partie la plus innovatrice de l'outil est qu'il a été conçu pour être employé par des programmeurs Java. Pour réduire la difficulté d'employer des techniques formelles, son objectif est de fournir une interface facile à utiliser qui cache aux utilisateurs la plupart des notions formelles et qui fournit une "vue Java" des lemmes.

Références :

Home page : http://www-sop.inria.fr/lemme/personnel/Lilian.Burdy/