GECCOO
Outils


Ergo projet ProVal, INRIA Futurs & LRI, Orsay Ergo est un outil de démonstration automatique dédié à la résolution d'obligations de preuve. Il utilise un algorithme de Congruence Closure paramétré par une théorie (actuellement l'arithmétique linéaire).
Genesyst LSR, Grenoble GénéSyst est un ensemble de classes utilisant la BoB (Boîte à outils B) pour générer des systèmes de transitions étiquetées représentant le comportement exact d'une spécification ou d'un raffinement B événementiel.
haRVey projet CASSIS, LORIA, Nancy-Besançon Un outil pour décider de la validité de formules du premier ordre modulo certaines théories equationnelles utiles à la preuve de programmes.
Jack Projet Everest, INRIA Sophia-Antipolis Un outil de vérification de programmes Java annoté par des spécifications JML développé initialement dans le laboratoire de recherche de Gemplus
JAG LIFC, Besançon Vérification de propriétés temporelles sur les classes Java avec JML
JML-Testing-Tools LIFC, Besançon Un animateur de spécifications JML
Krakatoa projet ProVal, INRIA Futurs & LRI, Orsay Un outil de vérification de programmes Java annoté par des spécifications JML
MECA Vasco, LSR Grenoble Un outil de génération de spécification d'opérations sécurisées sous forme de machines B à partir d'un modèle de politique de sécurité. d'accès

Ce document a t traduit de LATEX par HEVEA