- 2023
- David M. Russinoff:
A Formalization of Finite Group Theory: Part III. ACL2 2023: 33-49 - 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: 50-66 - Matt Kaufmann, J Strother Moore:
Advances in ACL2 Proof Debugging Tools. ACL2 2023: 67-81 - Ruben Gamboa, Panagiotis Manolios, Eric Whitman Smith, Kyle Thompson:
Using Counterexample Generation and Theory Exploration to Suggest Missing Hypotheses. ACL2 2023: 82-93 - Alessandro Coglio, Eric McCarthy, Eric Whitman Smith:
Formal Verification of Zero-Knowledge Circuits. ACL2 2023: 94-112 - Ankit Kumar, Max von Hippel, Panagiotis Manolios, Cristina Nita-Rotaru:
Verification of GossipSub in ACL2s. ACL2 2023: 113-132 - Andrew T. Walter, Ankit Kumar, Panagiotis Manolios:
Proving Calculational Proofs Correct. ACL2 2023: 133-150 - Grant O. Passmore:
ACL2 Proofs of Nonlinear Inequalities with Imandra. ACL2 2023: 151-160 - David S. Hardin:
Verification of a Rust Implementation of Knuth's Dancing Links using ACL2. ACL2 2023: 161-174 - David M. Russinoff:
A Formalization of Finite Group Theory: Part II. ACL2 2023: 16-32 - Alessandro Coglio, Sol Swords:
Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, TX, USA and online, November 13-14, 2023. EPTCS 393, 2023 [contents] - 2022
- Ruben Gamboa, Woodrow Gamboa:
All Prime Numbers Have Primitive Roots. ACL2 2022: 9-18 - Ruben Gamboa, Alicia Thoney:
Using ACL2 To Teach Students About Software Testing. ACL2 2022: 19-32 - 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: 33-47 - Warren A. Hunt Jr., Vivek Ramanathan, J Strother Moore:
VWSIM: A Circuit Simulator. ACL2 2022: 61-75 - Jagadish Bapanapally, Ruben Gamboa:
A Free Group of Rotations of Rank 2. ACL2 2022: 76-82 - William D. Young:
Modeling Asymptotic Complexity Using ACL2. ACL2 2022: 83-98 - Mertcan Temel
:
Verified Implementation of an Efficient Term-Rewriting Algorithm for Multiplier Verification on ACL2. ACL2 2022: 116-133 - Andrew T. Walter, Panagiotis Manolios
:
ACL2s Systems Programming. ACL2 2022: 134-150 - Alessandro Coglio, Eric McCarthy, Stephen J. Westfold, Daniel Balasubramanian
, Abhishek Dubey, Gabor Karsai:
Syntheto: A Surface Language for APT and ACL2. ACL2 2022: 151-167 - Alessandro Coglio:
A Complex Java Code Generator for ACL2 Based on a Shallow Embedding of ACL2 in Java. ACL2 2022: 168-184 - Alessandro Coglio:
A Proof-Generating C Code Generator for ACL2 Based on a Shallow Embedding of C in ACL2. ACL2 2022: 185-201 - David S. Hardin:
Hardware/Software Co-Assurance using the Rust Programming Language and ACL2. ACL2 2022: 202-216 - David M. Russinoff:
Properties of the Hebrew Calendar. ACL2 2022: 48-60 - David M. Russinoff:
A Formalization of Finite Group Theory. ACL2 2022: 99-115 - Rob Sumners, Cuong Chau:
Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022. EPTCS 359, 2022 [contents] - 2020
- David M. Russinoff:
Formal Verification of Arithmetic RTL: Translating Verilog to C++ to ACL2. ACL2 2020: 1-15 - Matt Kaufmann, J Strother Moore:
Iteration in ACL2. ACL2 2020: 16-31 - Sol Swords
:
New Rewriter Features in FGL. ACL2 2020: 32-46 - Rob Sumners:
Computing and Proving Well-founded Orderings through Finite Abstractions. ACL2 2020: 47-60