Français Anglais
Accueil Annuaire Plan du site
Accueil > Production scientifique > Logiciels et brevets
Production scientifique
[connexion sécurisée]
Logiciel Le Système HOL-Z


Le Système HOL-Z - Un système de preuve pour la Méthode Z
Date de dernière version : 16 juin 2008

Responsable : WOLFF Burkhart


HOL-Z est un système de preuve basé sur Isabelle/HOL (version 2005). Il est possible d'importer des specifications préparer en LaTeX et type-checked dans le système externe ZeTa. Le systeme genère des obligations de preuve pour l'analyse des spécifications et pour le raffinement d'un modele abstrait par
un modèle plus concrete (data refinement). Le système offre des moyens habituel d'Isabelle pour prouver ces obligations.

Pour en savoir plus: http://www.brucker.ch/projects/hol-z/

Logiciel - Licence : GPL



Activités de recherche
  Formalisation de langages (de spécification et de programmation) dans les assistants de preuve

Membres
  WOLFF Burkhart

Equipe
  Vérification d'Algorithmes, Langages et Systèmes

Logiciels et brevets
DATACERT
DataCert: A coq library for Data Intensive Languages and Systems Certification

PINT
Formal analysis of dynamics for large-scale biological networks

MAGMA
Contribution to numerical linear algebra libraries