Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
192 | Ruben Gamboa, John R. Cowles |
Implementing a cost-aware evaluator for ACL2 expressions. |
ACL2 |
2006 |
DBLP DOI BibTeX RDF |
ACL2 evaluator, function cost, evaluators |
178 | Warren A. Hunt Jr., Erik Reeber |
A SAT-based procedure for verifying finite state machines in ACL2. |
ACL2 |
2006 |
DBLP DOI BibTeX RDF |
satisfiability solving, theorem proving, hardware verification, ACL2 |
172 | Robert S. Boyer, Warren A. Hunt Jr. |
Function memoization and unique object representation for ACL2 functions. |
ACL2 |
2006 |
DBLP DOI BibTeX RDF |
ACL2 workshop, function memoization, hash CONS, hash CONSing, Lisp, ACL2 |
164 | Dale Vaillancourt, Rex L. Page, Matthias Felleisen |
ACL2 in DrScheme. |
ACL2 |
2006 |
DBLP DOI BibTeX RDF |
DrScheme, TeachScheme!, formal methods, pedagogy, ACL2 |
143 | Julien Schmaltz, Dominique Borrione |
Towards a formal theory of on chip communications in the ACL2 logic. |
ACL2 |
2006 |
DBLP DOI BibTeX RDF |
formal theory, network on a chip, theorem proving, communication theory |
143 | Lee Pike, Mark Shields, John Matthews |
A verifying core for a cryptographic language compiler. |
ACL2 |
2006 |
DBLP DOI BibTeX RDF |
cryptography, certification, optimizing compiler, ACL2, high-assurance, certifying compiler, verifying compiler |
136 | David L. Rager |
Adding parallelism capabilities to ACL2. |
ACL2 |
2006 |
DBLP DOI BibTeX RDF |
pand, parallel ACL2, pcall, plet, por, granularity, functional language |
136 | Jared Davis |
Reasoning about ACL2 file input. |
ACL2 |
2006 |
DBLP DOI BibTeX RDF |
UTF-8, file input, ACL2, unicode, exhaustive testing |
136 | Sol Swords, William R. Cook |
Soundness of the simply typed lambda calculus in ACL2. |
ACL2 |
2006 |
DBLP DOI BibTeX RDF |
lambda-calculus, soundness, ACL2 |
136 | Michael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds |
An embedding of the ACL2 logic in HOL. |
ACL2 |
2006 |
DBLP DOI BibTeX RDF |
HOL4, proof oracle, sound translation, verification, formal methods, logic, first-order logic, higher-order logic, ACL2, HOL |
132 | Michael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann |
An Integration of HOL and ACL2. |
FMCAD |
2006 |
DBLP DOI BibTeX RDF |
|
129 | Matt Kaufmann, J Strother Moore |
Double rewriting for equivalential reasoning in ACL2. |
ACL2 |
2006 |
DBLP DOI BibTeX RDF |
double-rewrite, verification, formal methods, rewriting, congruences, equivalence relations |
129 | David A. Greve |
Parameterized congruences in ACL2. |
ACL2 |
2006 |
DBLP DOI BibTeX RDF |
|
123 | Jared Davis |
Memories: array-like records for ACL2. |
ACL2 |
2006 |
DBLP DOI BibTeX RDF |
MBE, fixnum optimization, linear address spaces, arrays, records, ACL2 |
123 | John R. Cowles, Ruben Gamboa |
Unique factorization in ACL2: Euclidean domains. |
ACL2 |
2006 |
DBLP DOI BibTeX RDF |
Boyer-Moore logic, Euclidean domains, unique factorization, ACL2 |
119 | Warren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J Strother Moore, Eric Whitman Smith |
Meta Reasoning in ACL2. |
TPHOLs |
2005 |
DBLP DOI BibTeX RDF |
|
115 | Erik Reeber, Jun Sawada |
Combining ACL2 and an automated verification tool to verify a multiplier. |
ACL2 |
2006 |
DBLP DOI BibTeX RDF |
model checking, theorem proving, hardware verification |
115 | David S. Hardin, Eric W. Smith, William D. Young |
A robust machine code proof framework for highly secure applications. |
ACL2 |
2006 |
DBLP DOI BibTeX RDF |
cryptography, theorem proving, certification, symbolic simulation, ACL2, high-assurance, processor modeling |
112 | Carl Eastlund, Matthias Felleisen |
Making induction manifest in modular ACL2. |
PPDP |
2009 |
DBLP DOI BibTeX RDF |
theorem provers, acl2, module systems |
109 | David S. Hardin, Samuel S. Hardin |
ACL2 Meets the GPU: Formalizing a CUDA-based Parallelizable All-Pairs Shortest Path Algorithm in ACL2 |
ACL2 |
2013 |
DBLP DOI BibTeX RDF |
|
109 | Matt Kaufmann, J Strother Moore |
How Can I Do That with ACL2? Recent Enhancements to ACL2 |
ACL2 |
2011 |
DBLP DOI BibTeX RDF |
|
109 | Warren A. Hunt Jr., Serita M. Nelesen |
Phylogenetic trees in ACL2. |
ACL2 |
2006 |
DBLP DOI BibTeX RDF |
ACL2, phylogenetics |
105 | Peter C. Dillinger, Panagiotis Manolios, Daron Vroon 0001, J Strother Moore |
ACL2s: "The ACL2 Sedan". |
ICSE Companion |
2007 |
DBLP DOI BibTeX RDF |
|
105 | Warren A. Hunt Jr., Robert Bellarmine Krug, J Strother Moore |
Linear and Nonlinear Arithmetic in ACL2. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
101 | Sandip Ray |
Quantification in tail-recursive function definitions. |
ACL2 |
2006 |
DBLP DOI BibTeX RDF |
formal methods, logic, ACL2, conservativity, skolemization |
91 | Carl Eastlund, Matthias Felleisen |
Toward a Practical Module System for ACL2. |
PADL |
2009 |
DBLP DOI BibTeX RDF |
|
91 | Erik Reeber, Warren A. Hunt Jr. |
A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA). |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
87 | Alessandro Coglio |
A Complex Java Code Generator for ACL2 Based on a Shallow Embedding of ACL2 in Java. |
ACL2 |
2022 |
DBLP DOI BibTeX RDF |
|
87 | Alessandro Coglio |
A Proof-Generating C Code Generator for ACL2 Based on a Shallow Embedding of C in ACL2. |
ACL2 |
2022 |
DBLP DOI BibTeX RDF |
|
87 | Alessandro Coglio |
A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java. |
ACL2 |
2018 |
DBLP DOI BibTeX RDF |
|
87 | Jónathan Heras, Ekaterina Komendantskaya |
ACL2(ml): Machine-Learning for ACL2. |
ACL2 |
2014 |
DBLP DOI BibTeX RDF |
|
87 | Jared Davis, Sol Swords |
Verified AIG Algorithms in ACL2 |
ACL2 |
2013 |
DBLP DOI BibTeX RDF |
|
87 | Matt Kaufmann, J Strother Moore |
Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1 |
ACL2 |
2013 |
DBLP DOI BibTeX RDF |
|
87 | Caleb Eggensperger |
Proof Pad: A New Development Environment for ACL2 |
ACL2 |
2013 |
DBLP DOI BibTeX RDF |
|
87 | Peter Reid, Ruben Gamboa |
Implementing an Automatic Differentiator in ACL2 |
ACL2 |
2011 |
DBLP DOI BibTeX RDF |
|
87 | Sol Swords, Jared Davis |
Bit-Blasting ACL2 Theorems |
ACL2 |
2011 |
DBLP DOI BibTeX RDF |
|
87 | John R. Cowles, Ruben Gamboa |
Verifying Sierpinski and Riesel Numbers in ACL2 |
ACL2 |
2011 |
DBLP DOI BibTeX RDF |
|
79 | Tony Hoare |
The ideal of verified software. |
ACL2 |
2006 |
DBLP DOI BibTeX RDF |
|
77 | Ruben Gamboa, John R. Cowles |
Theory Extension in ACL2(r). |
J. Autom. Reason. |
2007 |
DBLP DOI BibTeX RDF |
Mathematics Subject Classifications (2000) 68T15, 03B35, 03H15 |
77 | J Strother Moore |
Finite Set Theory in ACL2. |
TPHOLs |
2001 |
DBLP DOI BibTeX RDF |
|
77 | Panagiotis Manolios, Sudarshan K. Srinivasan |
A Framework for Verifying Bit-Level Pipelined Machines Based on Automated Deduction and Decision Procedures. |
J. Autom. Reason. |
2006 |
DBLP DOI BibTeX RDF |
pipelined machines, bit-level, verification, refinement, automated reasoning, ACL2 |
77 | Panagiotis Manolios, Daron Vroon 0001 |
Ordinal Arithmetic: Algorithms and Mechanization. |
J. Autom. Reason. |
2005 |
DBLP DOI BibTeX RDF |
automated reasoning, arithmetic, ACL2, ordinal |
71 | Panagiotis Manolios, J Strother Moore |
Partial Functions in ACL2. |
J. Autom. Reason. |
2003 |
DBLP DOI BibTeX RDF |
ACL2, partial functions |
69 | Jun Sawada, Erik Reeber |
ACL2SIX: A Hint used to Integrate a Theorem Prover and an Automated Verification Tool. |
FMCAD |
2006 |
DBLP DOI BibTeX RDF |
|
69 | J Strother Moore |
Functional formal methods. |
ICFP |
2002 |
DBLP DOI BibTeX RDF |
functional programming, Java Virtual Machine, microarchitecture, software verification, Common Lisp, hardware verification, mechanical theorem proving |
66 | Matt Kaufmann, J Strother Moore |
Advances in ACL2 Proof Debugging Tools. |
ACL2 |
2023 |
DBLP DOI BibTeX RDF |
|
66 | Max von Hippel, Panagiotis Manolios, Kenneth L. McMillan, Cristina Nita-Rotaru, Lenore D. Zuck |
A Case Study in Analytic Protocol Analysis in ACL2. |
ACL2 |
2023 |
DBLP DOI BibTeX RDF |
|
66 | Grant O. Passmore |
ACL2 Proofs of Nonlinear Inequalities with Imandra. |
ACL2 |
2023 |
DBLP DOI BibTeX RDF |
|
66 | David S. Hardin |
Verification of a Rust Implementation of Knuth's Dancing Links using ACL2. |
ACL2 |
2023 |
DBLP DOI BibTeX RDF |
|
66 | Mertcan Temel |
Verified Implementation of an Efficient Term-Rewriting Algorithm for Multiplier Verification on ACL2. |
ACL2 |
2022 |
DBLP DOI BibTeX RDF |
|
66 | Alessandro Coglio, Eric McCarthy, Stephen J. Westfold, Daniel Balasubramanian, Abhishek Dubey, Gabor Karsai |
Syntheto: A Surface Language for APT and ACL2. |
ACL2 |
2022 |
DBLP DOI BibTeX RDF |
|
66 | Ruben Gamboa, Alicia Thoney |
Using ACL2 To Teach Students About Software Testing. |
ACL2 |
2022 |
DBLP DOI BibTeX RDF |
|
66 | David S. Hardin |
Hardware/Software Co-Assurance using the Rust Programming Language and ACL2. |
ACL2 |
2022 |
DBLP DOI BibTeX RDF |
|
66 | William D. Young |
Modeling Asymptotic Complexity Using ACL2. |
ACL2 |
2022 |
DBLP DOI BibTeX RDF |
|
66 | Alessandro Coglio |
Ethereum's Recursive Length Prefix in ACL2. |
ACL2 |
2020 |
DBLP DOI BibTeX RDF |
|
66 | Mertcan Temel |
RP-Rewriter: An Optimized Rewriter for Large Terms in ACL2. |
ACL2 |
2020 |
DBLP DOI BibTeX RDF |
|
66 | Ruben Gamboa, John R. Cowles, Woodrow Gamboa |
Quadratic Extensions in ACL2. |
ACL2 |
2020 |
DBLP DOI BibTeX RDF |
|
66 | David M. Russinoff |
Formal Verification of Arithmetic RTL: Translating Verilog to C++ to ACL2. |
ACL2 |
2020 |
DBLP DOI BibTeX RDF |
|
66 | Matt Kaufmann, J Strother Moore |
Iteration in ACL2. |
ACL2 |
2020 |
DBLP DOI BibTeX RDF |
|
66 | Carl Kwan, Mark R. Greenstreet |
Real Vector Spaces and the Cauchy-Schwarz Inequality in ACL2(r). |
ACL2 |
2018 |
DBLP DOI BibTeX RDF |
|
66 | Alessandro Coglio, Shilpi Goel |
Adding 32-bit Mode to the ACL2 Model of the x86 ISA. |
ACL2 |
2018 |
DBLP DOI BibTeX RDF |
|
66 | Carl Kwan, Mark R. Greenstreet |
Convex Functions in ACL2(r). |
ACL2 |
2018 |
DBLP DOI BibTeX RDF |
|
66 | Sol Swords |
Hint Orchestration Using ACL2's Simplifier. |
ACL2 |
2018 |
DBLP DOI BibTeX RDF |
|
66 | David S. Hardin, Konrad Slind |
Using ACL2 in the Design of Efficient, Verifiable Data Structures for High-Assurance Systems. |
ACL2 |
2018 |
DBLP DOI BibTeX RDF |
|
66 | Ruben Gamboa, John R. Cowles |
The Fundamental Theorem of Algebra in ACL2. |
ACL2 |
2018 |
DBLP DOI BibTeX RDF |
|
66 | Mihir Parang Mehta |
Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32. |
ACL2 |
2018 |
DBLP DOI BibTeX RDF |
|
66 | John R. Cowles, Ruben Gamboa |
The Cayley-Dickson Construction in ACL2. |
ACL2 |
2017 |
DBLP DOI BibTeX RDF |
|
66 | John R. Cowles, Ruben Gamboa |
Perfect Numbers in ACL2. |
ACL2 |
2015 |
DBLP DOI BibTeX RDF |
|
66 | Cuong K. Chau, Matt Kaufmann, Warren A. Hunt Jr. |
Fourier Series Formalization in ACL2(r). |
ACL2 |
2015 |
DBLP DOI BibTeX RDF |
|
66 | Alessandro Coglio |
Second-Order Functions and Theorems in ACL2. |
ACL2 |
2015 |
DBLP DOI BibTeX RDF |
|
66 | Yan Peng, Mark R. Greenstreet |
Extending ACL2 with SMT Solvers. |
ACL2 |
2015 |
DBLP DOI BibTeX RDF |
|
66 | Disha Puri, Sandip Ray, Kecheng Hao, Fei Xie |
Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis. |
ACL2 |
2014 |
DBLP DOI BibTeX RDF |
|
66 | Matt Kaufmann, J Strother Moore |
Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4. |
ACL2 |
2014 |
DBLP DOI BibTeX RDF |
|
66 | Jared Davis, Matt Kaufmann |
Industrial-Strength Documentation for ACL2. |
ACL2 |
2014 |
DBLP DOI BibTeX RDF |
|
66 | Sebastiaan J. C. Joosten, Cezary Kaliszyk, Josef Urban |
Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems. |
ACL2 |
2014 |
DBLP DOI BibTeX RDF |
|
66 | Harsh Raju Chamarthi, Peter C. Dillinger, Panagiotis Manolios |
Data Definitions in the ACL2 Sedan. |
ACL2 |
2014 |
DBLP DOI BibTeX RDF |
|
66 | Benjamin Selfridge, Eric Smith |
Polymorphic Types in ACL2. |
ACL2 |
2014 |
DBLP DOI BibTeX RDF |
|
66 | Benjamin Selfridge |
An ACL2 Mechanization of an Axiomatic Framework for Weak Memory. |
ACL2 |
2014 |
DBLP DOI BibTeX RDF |
|
66 | John W. O'Leary, David M. Russinoff |
Modeling Algorithms in SystemC and ACL2. |
ACL2 |
2014 |
DBLP DOI BibTeX RDF |
|
66 | David S. Hardin, Jennifer A. Davis, David A. Greve, Jedidiah R. McClurg |
Development of a Translator from LLVM to ACL2. |
ACL2 |
2014 |
DBLP DOI BibTeX RDF |
|
66 | Ruben Gamboa, Jared Davis (eds.) |
Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013. |
ACL2 |
2013 |
DBLP DOI BibTeX RDF |
|
66 | Bernard van Gastel, Julien Schmaltz |
A formalisation of XMAS |
ACL2 |
2013 |
DBLP DOI BibTeX RDF |
|
66 | David A. Greve, Konrad Slind |
A Step-Indexing Approach to Partial Functions |
ACL2 |
2013 |
DBLP DOI BibTeX RDF |
|
66 | Lucas Helms, Ruben Gamboa |
An Interpreter for Quantum Circuits |
ACL2 |
2013 |
DBLP DOI BibTeX RDF |
|
66 | Shilpi Goel, Warren A. Hunt Jr., Matt Kaufmann |
Abstract Stobjs and Their Application to ISA Modeling |
ACL2 |
2013 |
DBLP DOI BibTeX RDF |
|
66 | Sebastiaan J. C. Joosten, Bernard van Gastel, Julien Schmaltz |
A Macro for Reusing Abstract Functions and Theorems |
ACL2 |
2013 |
DBLP DOI BibTeX RDF |
|
66 | Freek Verbeek, Julien Schmaltz |
Verification of Building Blocks for Asynchronous Circuits |
ACL2 |
2013 |
DBLP DOI BibTeX RDF |
|
66 | David S. Hardin, Julien Schmaltz (eds.) |
Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011. |
ACL2 |
2011 |
DBLP DOI BibTeX RDF |
|
66 | Freek Verbeek, Julien Schmaltz |
Formal verification of a deadlock detection algorithm |
ACL2 |
2011 |
DBLP DOI BibTeX RDF |
|
66 | Peter-Michael Seidel |
Formal Verification of an Iterative Low-Power x86 Floating-Point Multiplier with Redundant Feedback |
ACL2 |
2011 |
DBLP DOI BibTeX RDF |
|
66 | Mike Dahlin, Ryan Johnson 0003, Robert Bellarmine Krug, Michael McCoyd, William D. Young |
Toward the Verification of a Simple Hypervisor |
ACL2 |
2011 |
DBLP DOI BibTeX RDF |
|
66 | Harsh Raju Chamarthi, Peter C. Dillinger, Matt Kaufmann, Panagiotis Manolios |
Integrating Testing and Interactive Theorem Proving |
ACL2 |
2011 |
DBLP DOI BibTeX RDF |
|
66 | Panagiotis Manolios, Matthew Wilding (eds.) |
Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006 |
ACL2 |
2006 |
DBLP BibTeX RDF |
|
63 | Matt Kaufmann, J Strother Moore |
An ACL2 Tutorial. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
63 | Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo, José-Luis Ruiz-Reina |
A Formal Proof of Dickson's Lemma in ACL2. |
LPAR |
2003 |
DBLP DOI BibTeX RDF |
|
63 | Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo, José-Luis Ruiz-Reina |
Formal Verification of Molecular Computational Models in ACL2: A Case Study. |
CAEPIA |
2003 |
DBLP DOI BibTeX RDF |
|
63 | José-Luis Ruiz-Reina, José Antonio Alonso Jimenez, María-José Hidalgo, Francisco-Jesús Martín-Mateos |
Formal Reasoning about Efficient Data Structures: A Case Study in ACL2. |
LOPSTR |
2003 |
DBLP DOI BibTeX RDF |
|
63 | Robert S. Boyer, J Strother Moore |
Single-Threaded Objects in ACL2. |
PADL |
2002 |
DBLP DOI BibTeX RDF |
|
63 | Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo, José-Luis Ruiz-Reina |
Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers. |
LOPSTR |
2002 |
DBLP DOI BibTeX RDF |
|
63 | José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo, Francisco-Jesús Martín-Mateos |
Formalizing Rewriting in the ACL2 Theorem Prover. |
AISC |
2000 |
DBLP DOI BibTeX RDF |
|