Paquet : alt-ergo (2.0.0-7 et autres)

[ Paquet source : alt-ergo  ]

démonstrateur automatique dédié à la vérification de programme

Alt-Ergo est un démonstrateur de théorème automatique dédié à la vérification de programme. Il est basé sur CC(X), un algorithme de clôture de congruence paramétré par une théorie équationnelle X. Alt-Ergo possède des démonstrateurs intégrés pour la logique propositionnelle, l’arithmétique linéaire, les symboles de fonctions non interprétées, les symboles de fonctions associatives/commutatives, des tableaux polymorphes, les types d’enregistrements polymorphes personnalisés et des types d’énumération polymorphes. Il possède une gestion restreinte pour raisonner sur des types d’algèbre personnalisés, des quantifieurs de premier ordre et de l’arithmétique non linéaire.

Ce paquet fournit le démonstrateur avec une interface en ligne de commande.

Étiquettes: Mis en œuvre en: OCaml, Interface utilisateur: Graphical User Interface, interface::x11, role::program, Boîte à outils d'interface utilisateur: GTK

Autres paquets associés à alt-ergo

• dep: libnum-ocaml-3st20

  paquet virtuel fourni par libnum-ocaml

• dep: libzarith-ocaml-6tqd3

  paquet virtuel fourni par libzarith-ocaml

• dep: libzip-ocaml-kb663

  paquet virtuel fourni par libzip-ocaml

• dep: ocaml-base-nox-4.11.1

  paquet virtuel fourni par ocaml-base-nox

• sug: why

  Paquet indisponible

Télécharger alt-ergo

Télécharger pour toutes les architectures proposées

Architecture	Version	Taille du paquet	Espace occupé une fois installé	Fichiers
armel	2.0.0-7+b4	282,7 ko	2 071,0 ko	[liste des fichiers]