Français Anglais
Accueil Annuaire Plan du site
Accueil > Production scientifique > Logiciels et brevets
Production scientifique
Logiciel Isabelle/HOL
Isabelle/HOL - Isabelle/HOL
Date de dernière version : 01 décembre 2013

Responsable : WENZEL Markus


Isabelle is one of the top five interactive theorem proving systems. It is used in numerous academic projects on formal theory development (Kepler Conjecture, Prime Number Theorem) and a few major industrial verifications (NICTA Verification of the L4 Kernel). Isabelle is jointly developed at University of Cambridge, Technische Universität München and Université Paris-Sud. The development at UPSud is focussed on the parallelization of the prover kernel and the development of asynchronous proof checking facilities and the development of new Prover IDE exploiting these features.

Pour en savoir plus: http://www.cl.cam.ac.uk/research/hvg/isabelle/

Logiciel - Licence : BSD License



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

Membres
  WENZEL Markus

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

Logiciels et brevets
TOUCHTOKENS
Low-cost Solution for Tangible Interfaces

LODATLAS
Browsing Linked Data Catalogs with LODAtlas

BOLDR
Query Intermediate Representation Library