- Referenced in 279 articles
- 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 Boyer-Moore family...
- Referenced in 33 articles
- Logic. This case study shows how non-ACL2 programs can be combined with ACL2 functions ... programs. Nothing is proved about the non-ACL2 programs Instead, the results ... ACL2 programs are checked at run time by ACL2 functions, and properties of these checker ... proving for first-order logic. The top ACL2 function takes a conjecture, preprocesses the conjecture...
- Referenced in 11 articles
- ACL2s: “the ACL2 sedan” ACL2 is the latest inception of the Boyer-Moore 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...
- Referenced in 20 articles
- Milawa is a theorem prover styled after ACL2 but with a small kernel...
- Referenced in 3 articles
- 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...
- Referenced in 2 articles
- 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...
- Referenced in 4 articles
- verification systems, such as ACL2, STEP, Tecton, and Simplify. On the other hand, obtaining...
- Referenced in 2 articles
- ACL2 LRAT checker. ”lrat” is mnemonic for ”Linear...
- Referenced in 1 article
- provers of the Boyer-Moore family like ACL2, and interactive proof assistants for typed higher...
- Referenced in 172 articles
- Axiom is a general purpose Computer Algebra system...
- Referenced in 1807 articles
- Coq is a formal proof management system. It...
- Referenced in 611 articles
- Isabelle is a generic proof assistant. It allows...
- Referenced in 51 articles
- LEO-II is a standalone, resolution-based higher...
- Referenced in 5124 articles
- The result of over 30 years of cutting...
- Referenced in 154 articles
- Maxima is a system for the manipulation of...
- Referenced in 145 articles
- The software system Theorema provides a uniform logic...
- Referenced in 71 articles
- TPS and ETPS are, respectively, the Theorem Proving...
- Referenced in 517 articles
- ML (’Meta Language’) is a general-purpose functional...
- Referenced in 233 articles
- COBOL (/ˈkoʊbɒl/, an acronym for common business-oriented...
- Referenced in 30 articles
- DrScheme is a programming environment for Scheme. It...