OSDN -- Développer et télécharger des logiciels Open Source
Traduction statut du Français translation status for fr

RSS
Télécharger la liste

Description du projet

ACL2 is a mathematical logic, programming
language, and mechanical theorem prover based on
the applicative subset of Common Lisp. It is an
"industrial-strength" version of the NQTHM or
Boyer/Moore theorem prover, and has been used for
the formal verification of commercial
microprocessors, the Java Virtual Machine,
interesting algorithms, and so forth.

Système requise

System requirement is not defined
Information regarding Project Releases and Project Resources. Note that the information here is a quote from Freecode.com page, and the downloads themselves may not be hosted on OSDN.

2006-12-05 09:07 Retour à la liste release
3.1

Une solidité quelques bugs ont été identifiés et corrigés ainsi que plusieurs erreurs Lisp potentiels durs ou d'autres problèmes mineurs. La performance des invariants de la théorie a été améliorée. Nouveaux livres inclure une résolution / prover paramodulation, modélisation simultanéité, l'induction transfinie et un utilitaire de simplification. Un nouveau «balise de confiance» permet l'usage d'éléments potentiellement dangereux dans les extensions ACL2.
Tags: Major bugfixes
A few soundness bugs were identified and corrected along with several potential hard Lisp errors and other minor issues. The performance of theory invariants has been improved. New books include a resolution/paramodulation prover, concurrency modelling, transfinite induction, and a simplification utility. A new "trust tag" feature allows the use of potentially unsafe features in ACL2 extensions.

Project Resources

Project Page Télécharger: Changelog Télécharger: Debian Package (deb) Télécharger: Demo Page d'accueil Télécharger: Liste Télécharger: TGZ