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.

2009-05-26 06:08
3.5

Il ya un support amélioré pour la commande de l'imprimante et «éviscération» de gros objets. Certificat fichiers maintenant tirer profit du partage de structure et sont plus compacts. L'utilisateur a maintenant davantage de contrôle sur les «gouvernants» utilisés dans l'analyse de résiliation. De nombreuses améliorations de l'efficacité diverses ont été faites, principalement en ce qui concerne l'appui de très grands objets. Une solidité quelques bugs ont été corrigé, et il ya eu de nombreuses autres corrections de bugs.
There is improved support for controlling the printer and "eviscerating" large objects. Certificate files now take advantage of structure sharing and are more compact. The user now has more control over the "rulers" used in termination analysis. Many various efficiency improvements have been made, mainly with respect to supporting very large objects. A few soundness bugs have been patched, and there have been numerous other bugfixes.

2007-06-05 23:51
3.2.1

Un bug bien-fondé et quelques autres bugs mineurs ont été corrigés. Y compris des livres a été accélérée par autant que 50%. Rewriting peut être dynamiquement contrôlée. Persistance accumulé appuie les règles-meta et identifie les règles inutiles, et de nombreuses autres mises à jour mineures ont été apportées.
Tags: Minor feature enhancements
A soundness bug and some other minor bugs have been fixed. Including books has been sped up by as much as 50%. Rewriting can be dynamically monitored. Accumulated persistence supports meta-rules and identifies useless rules, and many other minor updates have been made.

2006-12-05 09:07
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.

2006-08-06 06:07
3.0.1

Plusieurs bugs ont été corrigés, notamment un bug solidité. L'efficacité a été considérablement améliorée, et la suite de régression court environ 20% plus rapide. Les nouvelles fonctionnalités incluent des délais pour la cuve, des contrôles renforcés pour la compilation avec certifie-book, et un nouvel utilitaire pour le débogage a échoué encapsuler et progn événements.
Tags: Minor feature enhancements
Several bugs were fixed, including a soundness bug. Efficiency has been significantly improved, and the regression suite runs about 20% faster. New features include time limits for the prover, enhanced controls for compilation with certify-book, and a new utility for debugging failed encapsulate and progn events.

2006-06-01 09:54
3.0

Un nouveau make-métrages événement a été mis en place. C'est presque comme des macros qui prennent de l'Etat. Un meilleur soutien a été fourni pour: les règles de définition avec: expand hints. Désactivation de la vérification de la Garde a été ajouté. User-livres apportés sont désormais pris en charge, et une variété de fonctions ont été améliorées, y compris la vérification de la Garde impliquant termes terrain, théorie des invariants, et diabling événements defthm. Un bogue lié à la solidité de certains événements locaux a été fixé, ont des bugs mineurs liés à cw-gstack, humides, les événements embarquable, l'invite, arbres preuve, stobj impression, et: feuilletée.
Tags: Major feature enhancements
A new make-event feature was introduced. It is almost like macros that take state. Better support was provided for :definition rules with :expand hints. Disabling guard checking was added. User-contributed books are now supported, and a variety of features have been improved, including guard verification involving ground terms, theory invariants, and diabling defthm events. A soundness bug related to certain local events has been fixed, as have minor bugs related to cw-gstack, wet, embeddable events, the prompt, proof trees, stobj printing, and :puff.

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