- David S. Hardin:
Reasoning About LLVM Code Using Codewalker. ACL2 2015: 79-92 - Mitesh Jain, Panagiotis Manolios
:
Proving Skipping Refinement with ACL2s. ACL2 2015: 111-127 - J Strother Moore:
Stateman: Using Metafunctions to Manage Large Terms Representing Machine States. ACL2 2015: 93-109 - Yan Peng, Mark R. Greenstreet:
Extending ACL2 with SMT Solvers. ACL2 2015: 61-77 - Sol Swords, Jared Davis:
Fix Your Types. ACL2 2015: 3-16 - Matt Kaufmann, David L. Rager:
Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015. EPTCS 192, 2015 [contents] - 2014
- Harsh Raju Chamarthi, Peter C. Dillinger, Panagiotis Manolios:
Data Definitions in the ACL2 Sedan. ACL2 2014: 27-48 - John R. Cowles, Ruben Gamboa:
Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis. ACL2 2014: 89-100 - Jared Davis, Matt Kaufmann:
Industrial-Strength Documentation for ACL2. ACL2 2014: 9-25 - Ruben Gamboa, John R. Cowles:
Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent. ACL2 2014: 101-110 - David S. Hardin, Jennifer A. Davis, David A. Greve, Jedidiah R. McClurg:
Development of a Translator from LLVM to ACL2. ACL2 2014: 163-177 - Jónathan Heras, Ekaterina Komendantskaya:
ACL2(ml): Machine-Learning for ACL2. ACL2 2014: 61-75 - Sebastiaan J. C. Joosten, Cezary Kaliszyk, Josef Urban:
Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems. ACL2 2014: 77-85 - Matt Kaufmann, J Strother Moore:
Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4. ACL2 2014: 1-7 - John W. O'Leary, David M. Russinoff:
Modeling Algorithms in SystemC and ACL2. ACL2 2014: 145-162 - Disha Puri, Sandip Ray, Kecheng Hao, Fei Xie:
Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis. ACL2 2014: 111-128 - Benjamin Selfridge:
An ACL2 Mechanization of an Axiomatic Framework for Weak Memory. ACL2 2014: 129-144 - Benjamin Selfridge, Eric Smith:
Polymorphic Types in ACL2. ACL2 2014: 49-59 - Freek Verbeek, Julien Schmaltz:
Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014. EPTCS 152, 2014 [contents] - 2013
- Matt Kaufmann, J Strother Moore:
Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1. ACL2 2013: 5-12 - Caleb Eggensperger:
Proof Pad: A New Development Environment for ACL2. ACL2 2013: 13-28 - David A. Greve, Konrad Slind:
A Step-Indexing Approach to Partial Functions. ACL2 2013: 42-53 - Shilpi Goel, Warren A. Hunt Jr., Matt Kaufmann:
Abstract Stobjs and Their Application to ISA Modeling. ACL2 2013: 54-69 - Freek Verbeek, Julien Schmaltz:
Verification of Building Blocks for Asynchronous Circuits. ACL2 2013: 70-84 - Lucas Helms, Ruben Gamboa:
An Interpreter for Quantum Circuits. ACL2 2013: 85-94 - Jared Davis, Sol Swords:
Verified AIG Algorithms in ACL2. ACL2 2013: 95-110 - Bernard van Gastel, Julien Schmaltz:
A formalisation of XMAS. ACL2 2013: 111-126 - David S. Hardin, Samuel S. Hardin:
ACL2 Meets the GPU: Formalizing a CUDA-based Parallelizable All-Pairs Shortest Path Algorithm in ACL2. ACL2 2013: 127-142 - Sebastiaan J. C. Joosten, Bernard van Gastel, Julien Schmaltz:
A Macro for Reusing Abstract Functions and Theorems. ACL2 2013: 29-41 - Ruben Gamboa, Jared Davis:
Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013. EPTCS 114, 2013 [contents]
