
ACL2
 Referenced in 279 articles
[sw00060]
 ACL2 is both a programming language in which you can model computer systems ... help you prove properties of those models. ACL2 is part of the BoyerMoore family...

Ivy
 Referenced in 33 articles
[sw10279]
 Logic. This case study shows how nonACL2 programs can be combined with ACL2 functions ... programs. Nothing is proved about the nonACL2 programs Instead, the results ... ACL2 programs are checked at run time by ACL2 functions, and properties of these checker ... proving for firstorder logic. The top ACL2 function takes a conjecture, preprocesses the conjecture...

ACL2s
 Referenced in 11 articles
[sw07734]
 ACL2s: “the ACL2 sedan” ACL2 is the latest inception of the BoyerMoore theorem prover ... ever proved about commercially designed systems. Unfortunately, ACL2 has a steep learning curve. Thus, novices ... part of a project to make ACL2 and formal reasoning safe for the masses ... have developed ACL2s, the ACL2 sedan. ACL2s includes many features for streamlining the learning process...

Milawa
 Referenced in 20 articles
[sw09977]
 Milawa is a theorem prover styled after ACL2 but with a small kernel...

DrACuLa
 Referenced in 3 articles
[sw29646]
 DrACuLa  the programming environment for the ACL2 theorem prover in DrScheme: ACL2 in DrScheme. Teaching ... software in a formal framework such as ACL2 poses two immediate challenges. First, students typically ... applicative programming and are often unfamiliar with ACL2’s syntax. Second, for motivational reasons, students ... prove theorems about their games in ACL2. DRACULA provides a graphical front...

Proof Pad
 Referenced in 2 articles
[sw29644]
 Proof Pad: A New Development Environment for ACL2. Most software development projects rely on Integrated ... driven user interface. The standard installation of ACL2, on the other hand, is designed ... work closely with Emacs. ACL2 experts, on the whole, like this mode of operation ... discusses Proof Pad, a new IDE for ACL2. Proof Pad is not the only attempt...

RDL
 Referenced in 4 articles
[sw26677]
 verification systems, such as ACL2, STEP, Tecton, and Simplify. On the other hand, obtaining...

LRAT
 Referenced in 2 articles
[sw21570]
 ACL2 LRAT checker. ”lrat” is mnemonic for ”Linear...

Imandra
 Referenced in 1 article
[sw37911]
 provers of the BoyerMoore family like ACL2, and interactive proof assistants for typed higher...

AXIOM
 Referenced in 172 articles
[sw00063]
 Axiom is a general purpose Computer Algebra system...

Coq
 Referenced in 1807 articles
[sw00161]
 Coq is a formal proof management system. It...

Isabelle
 Referenced in 611 articles
[sw00454]
 Isabelle is a generic proof assistant. It allows...

LEOII
 Referenced in 51 articles
[sw00512]
 LEOII is a standalone, resolutionbased higher...

Maple
 Referenced in 5124 articles
[sw00545]
 The result of over 30 years of cutting...

Maxima
 Referenced in 154 articles
[sw00560]
 Maxima is a system for the manipulation of...

Theorema
 Referenced in 145 articles
[sw00961]
 The software system Theorema provides a uniform logic...

TPS
 Referenced in 71 articles
[sw00973]
 TPS and ETPS are, respectively, the Theorem Proving...

ML
 Referenced in 517 articles
[sw01218]
 ML (’Meta Language’) is a generalpurpose functional...

COBOL
 Referenced in 233 articles
[sw01228]
 COBOL (/ˈkoʊbɒl/, an acronym for common businessoriented...

DrScheme
 Referenced in 30 articles
[sw01265]
 DrScheme is a programming environment for Scheme. It...