Etat de l’art : Travaux formels
Preuve de la sûreté des types en Java
2 approches:
- source
- ? sous-ens. Java séquentiels ? prouver préservation des types [Drossopoulou, Eisenbach, Syme]
- Empilement de ? sous-ens Java pour sém. dynamique [Börger, Schultze]
- byte code
- Transitions d’états d’un sous-ens. des instructions de la JVM [Qian] dans la mémoire qd. exécution ? prouver bon fonctionnement
- Systèmes à états finis pour vérif. de byte code Java Card [Posegga, Vogt]
- Procédure de vérif. de la sûreté du byte-code sur un sous-ens. [Rose]