| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Alessandro Coglio, Sol Swords (eds.) |
Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, TX, USA and online, November 13-14, 2023.  |
ACL2  |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Matt Kaufmann, J Strother Moore |
Advances in ACL2 Proof Debugging Tools. |
ACL2 |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew T. Walter, Ankit Kumar, Panagiotis Manolios |
Proving Calculational Proofs Correct. |
ACL2 |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Coglio, Eric McCarthy, Eric W. Smith |
Formal Verification of Zero-Knowledge Circuits. |
ACL2 |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | David M. Russinoff |
A Formalization of Finite Group Theory: Part III. |
ACL2 |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
|
| 1 | David M. Russinoff |
A Formalization of Finite Group Theory: Part II. |
ACL2 |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Ruben Gamboa, Panagiotis Manolios, Eric Whitman Smith, Kyle Thompson |
Using Counterexample Generation and Theory Exploration to Suggest Missing Hypotheses. |
ACL2 |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Grant O. Passmore |
ACL2 Proofs of Nonlinear Inequalities with Imandra. |
ACL2 |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | David S. Hardin |
Verification of a Rust Implementation of Knuth's Dancing Links using ACL2. |
ACL2 |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Ankit Kumar, Max von Hippel, Panagiotis Manolios, Cristina Nita-Rotaru |
Verification of GossipSub in ACL2s. |
ACL2 |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Mertcan Temel |
Verified Implementation of an Efficient Term-Rewriting Algorithm for Multiplier Verification on ACL2. |
ACL2 |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Ruben Gamboa, Woodrow Gamboa |
All Prime Numbers Have Primitive Roots. |
ACL2 |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Jagadish Bapanapally, Ruben Gamboa |
A Free Group of Rotations of Rank 2. |
ACL2 |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
|
| 1 | Alessandro Coglio |
A Complex Java Code Generator for ACL2 Based on a Shallow Embedding of ACL2 in Java. |
ACL2 |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | David M. Russinoff |
Properties of the Hebrew Calendar. |
ACL2 |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Warren A. Hunt Jr., Vivek Ramanathan, J Strother Moore |
VWSIM: A Circuit Simulator. |
ACL2 |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Rob Sumners, Cuong Chau (eds.) |
Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022. |
ACL2 |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Ruben Gamboa, Alicia Thoney |
Using ACL2 To Teach Students About Software Testing. |
ACL2 |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | David S. Hardin |
Hardware/Software Co-Assurance using the Rust Programming Language and ACL2. |
ACL2 |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
|
| 1 | William D. Young |
Modeling Asymptotic Complexity Using ACL2. |
ACL2 |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew T. Walter, Panagiotis Manolios |
ACL2s Systems Programming. |
ACL2 |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | David A. Greve, Jennifer A. Davis, Laura R. Humphrey |
A Mechanized Proof of Bounded Convergence Time for the Distributed Perimeter Surveillance System (DPSS) Algorithm A. |
ACL2 |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | David M. Russinoff |
A Formalization of Finite Group Theory. |
ACL2 |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Coglio |
Ethereum's Recursive Length Prefix in ACL2. |
ACL2 |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Mertcan Temel |
RP-Rewriter: An Optimized Rewriter for Large Terms in ACL2. |
ACL2 |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Rob Sumners |
Computing and Proving Well-founded Orderings through Finite Abstractions. |
ACL2 |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Ruben Gamboa, John R. Cowles, Woodrow Gamboa |
Quadratic Extensions in ACL2. |
ACL2 |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | David M. Russinoff |
Formal Verification of Arithmetic RTL: Translating Verilog to C++ to ACL2. |
ACL2 |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Sol Swords |
New Rewriter Features in FGL. |
ACL2 |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Sol Swords |
Generating Mutually Inductive Theorems from Concise Descriptions. |
ACL2 |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Matt Kaufmann, J Strother Moore |
Iteration in ACL2. |
ACL2 |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Grant O. Passmore, Ruben Gamboa (eds.) |
Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications, Worldwide, Planet Earth, May 28-29, 2020. |
ACL2 |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Coglio, Stephen J. Westfold |
Isomorphic Data Type Transformations. |
ACL2 |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Carl Kwan, Mark R. Greenstreet |
Real Vector Spaces and the Cauchy-Schwarz Inequality in ACL2(r). |
ACL2 |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | David A. Greve, Andrew Gacek |
Trapezoidal Generalization over Linear Constraints. |
ACL2 |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Coglio, Shilpi Goel |
Adding 32-bit Mode to the ACL2 Model of the x86 ISA. |
ACL2 |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Matt Kaufmann |
DefunT: A Tool for Automating Termination Proofs by Using the Community Books (Extended Abstract). |
ACL2 |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Carl Kwan, Mark R. Greenstreet |
Convex Functions in ACL2(r). |
ACL2 |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Sol Swords |
Hint Orchestration Using ACL2's Simplifier. |
ACL2 |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Shilpi Goel, Matt Kaufmann (eds.) |
Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018. |
ACL2 |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Yan Peng, Mark R. Greenstreet |
Smtlink 2.0. |
ACL2 |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Sol Swords |
Incremental SAT Library Integration Using Abstract Stobjs. |
ACL2 |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
|
| 1 | Ruben Gamboa, John R. Cowles |
The Fundamental Theorem of Algebra in ACL2. |
ACL2 |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Coglio |
A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java. |
ACL2 |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Mihir Parang Mehta |
Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32. |
ACL2 |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Rob Sumners |
Proof Reduction of Fair Stuttering Refinement of Asynchronous Systems and Applications. |
ACL2 |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | John R. Cowles, Ruben Gamboa |
The Cayley-Dickson Construction in ACL2. |
ACL2 |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Sol Swords |
Term-Level Reasoning in Support of Bit-blasting. |
ACL2 |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Matt Kaufmann, Sol Swords |
Meta-extract: Using Existing Facts in Meta-reasoning. |
ACL2 |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Anna Slobodová, Warren A. Hunt Jr. (eds.) |
Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, May 22-23, 2017. |
ACL2 |
2017 |
DBLP BibTeX RDF |
|
| 1 | David M. Russinoff |
A Computationally Surveyable Proof of the Group Properties of an Elliptic Curve. |
ACL2 |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Coglio, Matt Kaufmann, Eric Whitman Smith |
A Versatile, Sound Tool for Simplifying Definitions. |
ACL2 |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Shilpi Goel |
The x86isa Books: Features, Usage, and Future Plans. |
ACL2 |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | David S. Hardin |
Reasoning About LLVM Code Using Codewalker. |
ACL2 |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | John R. Cowles, Ruben Gamboa |
Perfect Numbers in ACL2. |
ACL2 |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | J Strother Moore |
Stateman: Using Metafunctions to Manage Large Terms Representing Machine States. |
ACL2 |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Cuong K. Chau, Matt Kaufmann, Warren A. Hunt Jr. |
Fourier Series Formalization in ACL2(r). |
ACL2 |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Mitesh Jain, Panagiotis Manolios |
Proving Skipping Refinement with ACL2s. |
ACL2 |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Sol Swords, Jared Davis |
Fix Your Types. |
ACL2 |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Coglio |
Second-Order Functions and Theorems in ACL2. |
ACL2 |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Yan Peng, Mark R. Greenstreet |
Extending ACL2 with SMT Solvers. |
ACL2 |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Matt Kaufmann, David L. Rager (eds.) |
Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015. |
ACL2 |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Disha Puri, Sandip Ray, Kecheng Hao, Fei Xie |
Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis. |
ACL2 |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Matt Kaufmann, J Strother Moore |
Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4. |
ACL2 |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Jared Davis, Matt Kaufmann |
Industrial-Strength Documentation for ACL2. |
ACL2 |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
|
| 1 | Harsh Raju Chamarthi, Peter C. Dillinger, Panagiotis Manolios |
Data Definitions in the ACL2 Sedan. |
ACL2 |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Jónathan Heras, Ekaterina Komendantskaya |
ACL2(ml): Machine-Learning for ACL2. |
ACL2 |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Ruben Gamboa, John R. Cowles |
Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent. |
ACL2 |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Benjamin Selfridge, Eric Smith |
Polymorphic Types in ACL2. |
ACL2 |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | John R. Cowles, Ruben Gamboa |
Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis. |
ACL2 |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Benjamin Selfridge |
An ACL2 Mechanization of an Axiomatic Framework for Weak Memory. |
ACL2 |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Freek Verbeek, Julien Schmaltz (eds.) |
Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014. |
ACL2 |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | John W. O'Leary, David M. Russinoff |
Modeling Algorithms in SystemC and ACL2. |
ACL2 |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
|
| 1 | Jared Davis, Sol Swords |
Verified AIG Algorithms in ACL2 |
ACL2 |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Matt Kaufmann, J Strother Moore |
Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1 |
ACL2 |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Bernard van Gastel, Julien Schmaltz |
A formalisation of XMAS |
ACL2 |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Caleb Eggensperger |
Proof Pad: A New Development Environment for ACL2 |
ACL2 |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | David A. Greve, Konrad Slind |
A Step-Indexing Approach to Partial Functions |
ACL2 |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Lucas Helms, Ruben Gamboa |
An Interpreter for Quantum Circuits |
ACL2 |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Shilpi Goel, Warren A. Hunt Jr., Matt Kaufmann |
Abstract Stobjs and Their Application to ISA Modeling |
ACL2 |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Sebastiaan J. C. Joosten, Bernard van Gastel, Julien Schmaltz |
A Macro for Reusing Abstract Functions and Theorems |
ACL2 |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
|
| 1 | Freek Verbeek, Julien Schmaltz |
Verification of Building Blocks for Asynchronous Circuits |
ACL2 |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
|
| 1 | Freek Verbeek, Julien Schmaltz |
Formal verification of a deadlock detection algorithm |
ACL2 |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
|
| 1 | Peter Reid, Ruben Gamboa |
Implementing an Automatic Differentiator in ACL2 |
ACL2 |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Sol Swords, Jared Davis |
Bit-Blasting ACL2 Theorems |
ACL2 |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Matt Kaufmann, J Strother Moore |
How Can I Do That with ACL2? Recent Enhancements to ACL2 |
ACL2 |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter-Michael Seidel |
Formal Verification of an Iterative Low-Power x86 Floating-Point Multiplier with Redundant Feedback |
ACL2 |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
|
| 1 | John R. Cowles, Ruben Gamboa |
Verifying Sierpinski and Riesel Numbers in ACL2 |
ACL2 |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Harsh Raju Chamarthi, Peter C. Dillinger, Matt Kaufmann, Panagiotis Manolios |
Integrating Testing and Interactive Theorem Proving |
ACL2 |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | David L. Rager |
Adding parallelism capabilities to ACL2. |
ACL2 |
2006 |
DBLP DOI BibTeX RDF |
pand, parallel ACL2, pcall, plet, por, granularity, functional language |
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license