toutes les options
jessie  ] [  stretch  ] [  buster  ] [  bullseye  ] [  sid  ]
[ Paquet source : alt-ergo  ]

Paquet : alt-ergo (2.0.0-3)

Liens pour alt-ergo

Screenshot

Ressources Debian :

Télécharger le paquet source alt-ergo :

Responsables :

Ressources externes :

Paquets similaires :

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és, 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 des interfaces en ligne de commande et graphique.

É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

  • dépendances
  • recommandations
  • suggestions
  • enhances

Télécharger alt-ergo

Télécharger pour toutes les architectures proposées
Architecture Taille du paquet Espace occupé une fois installé Fichiers
armel 395,6 ko4 505,0 ko [liste des fichiers]