| 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 |