Résumé:
Je présente mon expérience récente avec Spike, un démonstrateur
automatique basé sur la récurrence, concernant la vérification des
diagrames de commutation des machines défensive et offensive pour
JavaCard. Dans un premier temps, je vais introduire le concept de
preuve par récurrence de Spike, ainsi que son systeme d'inférence. Puis, je
présente les extensions de Spike afin de répondre aux problèmes
particuliers liés à la spécification et la vérification du code JavaCard.
Abstract:
I will present my new experience with Spike, an induction-based
automatic prover, concerning the verification of the commuting
diagrams for the offensive and defensive JavaCard machines. Firstly, I
will introduce the induction proof concept of Spike, together with its
inference system. Then, I will show some extensions to it needed to
specify and verify the JavaCard code.
Retour au sommaire / Back to schedule