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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Matt Kaufmann, J Strother Moore |
Advances in ACL2 Proof Debugging Tools. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, TX, USA and online, November 13-14, 2023., pp. 67-81, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Andrew T. Walter, Ankit Kumar, Panagiotis Manolios |
Proving Calculational Proofs Correct. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, TX, USA and online, November 13-14, 2023., pp. 133-150, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Alessandro Coglio, Eric McCarthy, Eric W. Smith |
Formal Verification of Zero-Knowledge Circuits. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, TX, USA and online, November 13-14, 2023., pp. 94-112, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | David M. Russinoff |
A Formalization of Finite Group Theory: Part III. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, TX, USA and online, November 13-14, 2023., pp. 33-49, 2023. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, TX, USA and online, November 13-14, 2023., pp. 50-66, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | David M. Russinoff |
A Formalization of Finite Group Theory: Part II. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, TX, USA and online, November 13-14, 2023., pp. 16-32, 2023. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, TX, USA and online, November 13-14, 2023., pp. 82-93, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Grant O. Passmore |
ACL2 Proofs of Nonlinear Inequalities with Imandra. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, TX, USA and online, November 13-14, 2023., pp. 151-160, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | David S. Hardin |
Verification of a Rust Implementation of Knuth's Dancing Links using ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, TX, USA and online, November 13-14, 2023., pp. 161-174, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Ankit Kumar, Max von Hippel, Panagiotis Manolios, Cristina Nita-Rotaru |
Verification of GossipSub in ACL2s. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, TX, USA and online, November 13-14, 2023., pp. 113-132, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Mertcan Temel |
Verified Implementation of an Efficient Term-Rewriting Algorithm for Multiplier Verification on ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022., pp. 116-133, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Ruben Gamboa, Woodrow Gamboa |
All Prime Numbers Have Primitive Roots. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022., pp. 9-18, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Jagadish Bapanapally, Ruben Gamboa |
A Free Group of Rotations of Rank 2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022., pp. 76-82, 2022. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022., pp. 151-167, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Alessandro Coglio |
A Complex Java Code Generator for ACL2 Based on a Shallow Embedding of ACL2 in Java. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022., pp. 168-184, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | David M. Russinoff |
Properties of the Hebrew Calendar. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022., pp. 48-60, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Warren A. Hunt Jr., Vivek Ramanathan, J Strother Moore |
VWSIM: A Circuit Simulator. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022., pp. 61-75, 2022. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Ruben Gamboa, Alicia Thoney |
Using ACL2 To Teach Students About Software Testing. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022., pp. 19-32, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | David S. Hardin |
Hardware/Software Co-Assurance using the Rust Programming Language and ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022., pp. 202-216, 2022. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022., pp. 185-201, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | William D. Young |
Modeling Asymptotic Complexity Using ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022., pp. 83-98, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Andrew T. Walter, Panagiotis Manolios |
ACL2s Systems Programming. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022., pp. 134-150, 2022. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022., pp. 33-47, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | David M. Russinoff |
A Formalization of Finite Group Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022., pp. 99-115, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Alessandro Coglio |
Ethereum's Recursive Length Prefix in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications, Worldwide, Planet Earth, May 28-29, 2020., pp. 108-124, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
1 | Mertcan Temel |
RP-Rewriter: An Optimized Rewriter for Large Terms in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications, Worldwide, Planet Earth, May 28-29, 2020., pp. 61-74, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
1 | Rob Sumners |
Computing and Proving Well-founded Orderings through Finite Abstractions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications, Worldwide, Planet Earth, May 28-29, 2020., pp. 47-60, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
1 | Ruben Gamboa, John R. Cowles, Woodrow Gamboa |
Quadratic Extensions in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications, Worldwide, Planet Earth, May 28-29, 2020., pp. 75-86, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
1 | David M. Russinoff |
Formal Verification of Arithmetic RTL: Translating Verilog to C++ to ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications, Worldwide, Planet Earth, May 28-29, 2020., pp. 1-15, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
1 | Sol Swords |
New Rewriter Features in FGL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications, Worldwide, Planet Earth, May 28-29, 2020., pp. 32-46, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
1 | Sol Swords |
Generating Mutually Inductive Theorems from Concise Descriptions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications, Worldwide, Planet Earth, May 28-29, 2020., pp. 95-107, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
1 | Matt Kaufmann, J Strother Moore |
Iteration in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications, Worldwide, Planet Earth, May 28-29, 2020., pp. 16-31, 2020. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
1 | Alessandro Coglio, Stephen J. Westfold |
Isomorphic Data Type Transformations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications, Worldwide, Planet Earth, May 28-29, 2020., pp. 125-141, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
1 | Carl Kwan, Mark R. Greenstreet |
Real Vector Spaces and the Cauchy-Schwarz Inequality in ACL2(r). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018., pp. 111-127, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | David A. Greve, Andrew Gacek |
Trapezoidal Generalization over Linear Constraints. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018., pp. 30-46, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Alessandro Coglio, Shilpi Goel |
Adding 32-bit Mode to the ACL2 Model of the x86 ISA. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018., pp. 77-94, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Matt Kaufmann |
DefunT: A Tool for Automating Termination Proofs by Using the Community Books (Extended Abstract). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018., pp. 161-163, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Carl Kwan, Mark R. Greenstreet |
Convex Functions in ACL2(r). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018., pp. 128-142, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Sol Swords |
Hint Orchestration Using ACL2's Simplifier. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018., pp. 164-171, 2018. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Yan Peng, Mark R. Greenstreet |
Smtlink 2.0. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018., pp. 143-160, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Sol Swords |
Incremental SAT Library Integration Using Abstract Stobjs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018., pp. 47-60, 2018. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018., pp. 61-76, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Ruben Gamboa, John R. Cowles |
The Fundamental Theorem of Algebra in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018., pp. 98-110, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Alessandro Coglio |
A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018., pp. 1-17, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Mihir Parang Mehta |
Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018., pp. 18-29, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Rob Sumners |
Proof Reduction of Fair Stuttering Refinement of Asynchronous Systems and Applications. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, May 22-23, 2017., pp. 78-94, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | John R. Cowles, Ruben Gamboa |
The Cayley-Dickson Construction in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, May 22-23, 2017., pp. 18-29, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Sol Swords |
Term-Level Reasoning in Support of Bit-blasting. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, May 22-23, 2017., pp. 95-111, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Matt Kaufmann, Sol Swords |
Meta-extract: Using Existing Facts in Meta-reasoning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, May 22-23, 2017., pp. 47-60, 2017. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP BibTeX RDF |
|
1 | David M. Russinoff |
A Computationally Surveyable Proof of the Group Properties of an Elliptic Curve. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, May 22-23, 2017., pp. 30-46, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Alessandro Coglio, Matt Kaufmann, Eric Whitman Smith |
A Versatile, Sound Tool for Simplifying Definitions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, May 22-23, 2017., pp. 61-77, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Shilpi Goel |
The x86isa Books: Features, Usage, and Future Plans. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, May 22-23, 2017., pp. 1-17, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | David S. Hardin |
Reasoning About LLVM Code Using Codewalker. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015., pp. 79-92, 2015. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
1 | John R. Cowles, Ruben Gamboa |
Perfect Numbers in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015., pp. 53-59, 2015. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
1 | J Strother Moore |
Stateman: Using Metafunctions to Manage Large Terms Representing Machine States. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015., pp. 93-109, 2015. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Cuong K. Chau, Matt Kaufmann, Warren A. Hunt Jr. |
Fourier Series Formalization in ACL2(r). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015., pp. 35-51, 2015. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Mitesh Jain, Panagiotis Manolios |
Proving Skipping Refinement with ACL2s. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015., pp. 111-127, 2015. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Sol Swords, Jared Davis |
Fix Your Types. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015., pp. 3-16, 2015. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Alessandro Coglio |
Second-Order Functions and Theorems in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015., pp. 17-33, 2015. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Yan Peng, Mark R. Greenstreet |
Extending ACL2 with SMT Solvers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015., pp. 61-77, 2015. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Disha Puri, Sandip Ray, Kecheng Hao, Fei Xie |
Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014., pp. 111-128, 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Matt Kaufmann, J Strother Moore |
Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014., pp. 1-7, 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Jared Davis, Matt Kaufmann |
Industrial-Strength Documentation for ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014., pp. 9-25, 2014. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014., pp. 77-85, 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Harsh Raju Chamarthi, Peter C. Dillinger, Panagiotis Manolios |
Data Definitions in the ACL2 Sedan. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014., pp. 27-48, 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Jónathan Heras, Ekaterina Komendantskaya |
ACL2(ml): Machine-Learning for ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014., pp. 61-75, 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Ruben Gamboa, John R. Cowles |
Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014., pp. 101-110, 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Benjamin Selfridge, Eric Smith |
Polymorphic Types in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014., pp. 49-59, 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
1 | John R. Cowles, Ruben Gamboa |
Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014., pp. 89-100, 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Benjamin Selfridge |
An ACL2 Mechanization of an Axiomatic Framework for Weak Memory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014., pp. 129-144, 2014. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
1 | John W. O'Leary, David M. Russinoff |
Modeling Algorithms in SystemC and ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014., pp. 145-162, 2014. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014., pp. 163-177, 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Jared Davis, Sol Swords |
Verified AIG Algorithms in ACL2 ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013., pp. 95-110, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Matt Kaufmann, J Strother Moore |
Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1 ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013., pp. 5-12, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Bernard van Gastel, Julien Schmaltz |
A formalisation of XMAS ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013., pp. 111-126, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Caleb Eggensperger |
Proof Pad: A New Development Environment for ACL2 ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013., pp. 13-28, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
1 | David A. Greve, Konrad Slind |
A Step-Indexing Approach to Partial Functions ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013., pp. 42-53, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Lucas Helms, Ruben Gamboa |
An Interpreter for Quantum Circuits ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013., pp. 85-94, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Shilpi Goel, Warren A. Hunt Jr., Matt Kaufmann |
Abstract Stobjs and Their Application to ISA Modeling ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013., pp. 54-69, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Sebastiaan J. C. Joosten, Bernard van Gastel, Julien Schmaltz |
A Macro for Reusing Abstract Functions and Theorems ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013., pp. 29-41, 2013. The full citation details ...](Pics/full.jpeg) |
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 ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013., pp. 127-142, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Freek Verbeek, Julien Schmaltz |
Verification of Building Blocks for Asynchronous Circuits ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013., pp. 70-84, 2013. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Freek Verbeek, Julien Schmaltz |
Formal verification of a deadlock detection algorithm ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011., pp. 103-112, 2011. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Peter Reid, Ruben Gamboa |
Implementing an Automatic Differentiator in ACL2 ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011., pp. 61-69, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Sol Swords, Jared Davis |
Bit-Blasting ACL2 Theorems ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011., pp. 84-102, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Matt Kaufmann, J Strother Moore |
How Can I Do That with ACL2? Recent Enhancements to ACL2 ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011., pp. 46-60, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Peter-Michael Seidel |
Formal Verification of an Iterative Low-Power x86 Floating-Point Multiplier with Redundant Feedback ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011., pp. 70-83, 2011. The full citation details ...](Pics/full.jpeg) |
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 ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011., pp. 28-45, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | John R. Cowles, Ruben Gamboa |
Verifying Sierpinski and Riesel Numbers in ACL2 ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011., pp. 20-27, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Harsh Raju Chamarthi, Peter C. Dillinger, Matt Kaufmann, Panagiotis Manolios |
Integrating Testing and Interactive Theorem Proving ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011., pp. 4-19, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | David L. Rager |
Adding parallelism capabilities to ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006, pp. 90-94, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
pand, parallel ACL2, pcall, plet, por, granularity, functional language |