Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
57 | Ruben A. Gamboa |
A Formalization of Powerlist Algebra in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 43(2), pp. 139-172, 2009. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
Powerlists, Verification, ACL2 |
57 | Matt Kaufmann |
Verification of Year 2000 conversion rules using the ACL2 theorem prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Softw. Tools Technol. Transf. ![In: Int. J. Softw. Tools Technol. Transf. 3(1), pp. 13-19, 2000. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
Formal verification, Program transformation, Automated reasoning, ACL2, Year 2000 |
55 | Warren A. Hunt Jr., Sol Swords |
Centaur Technology Media Unit Verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV ![In: Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, pp. 353-367, 2009, Springer, 978-3-642-02657-7. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
49 | Bishop Brock, Matt Kaufmann, J Strother Moore |
Rewriting with Equivalence Relations in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 40(4), pp. 293-306, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
Refinement, Rewriting, Congruence, Equivalence relations |
49 | James Reynolds |
Automatically Translating Type and Function Definitions from HOL to ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings, pp. 262-277, 2007, Springer, 978-3-540-74590-7. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
49 | Mirian Andrés, Laureano Lambán, Julio Rubio 0001 |
Executing in Common Lisp, Proving in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Calculemus/MKM ![In: Towards Mechanized Mathematical Assistants, 14th Symposium, Calculemus 2007, 6th International Conference, MKM 2007, Hagenberg, Austria, June 27-30, 2007, Proceedings, pp. 1-12, 2007, Springer, 978-3-540-73083-5. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
49 | Diana Toma, Dominique Borrione |
Formal Verification of a SHA-1 Circuit Core Using ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, pp. 326-341, 2005, Springer, 3-540-28372-2. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
49 | Yann Zimmermann, Diana Toma |
Component Reuse in B Using ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ZB ![In: ZB 2005: Formal Specification and Development in Z and B, 4th International Conference of B and Z Users, Guildford, UK, April 13-15, 2005, Proceedings, pp. 279-298, 2005, Springer, 3-540-25559-1. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
49 | Panagiotis Manolios, Daron Vroon 0001 |
Integrating Reasoning About Ordinal Arithmetic into ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMCAD ![In: Formal Methods in Computer-Aided Design, 5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings, pp. 82-97, 2004, Springer, 3-540-23738-0. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
49 | Magali Contensin, Laurence Pierre |
Combining ACL2 and a v-calculus Model-Checker to Verify System-Level Designs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MEMOCODE ![In: 1st ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2003), 24-26 June 2003, Mont Saint-Michel, France, Proceedings, pp. 75-, 2003, IEEE Computer Society, 0-7695-1923-7. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
49 | David M. Russinoff |
A Case Study in Fomal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD AthlonTM Processor. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMCAD ![In: Formal Methods in Computer-Aided Design, Third International Conference, FMCAD 2000, Austin, Texas, USA, November 1-3, 2000, Proceedings, pp. 3-36, 2000, Springer, 3-540-41219-0. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
49 | Matt Kaufmann |
ACL2 Support for Verification Projects (Invited Talk). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings, pp. 220-238, 1998, Springer, 3-540-64675-2. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
49 | Sandip Ray, Rob Sumners |
Combining Theorem Proving with Model Checking through Predicate Abstraction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Des. Test Comput. ![In: IEEE Des. Test Comput. 24(2), pp. 132-139, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
model checking, formal verification, theorem proving, predicate abstraction, ACL2 |
49 | José-Luis Ruiz-Reina, Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo |
Formal Correctness of a Quadratic Unification Algorithm. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 37(1-2), pp. 67-92, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
verification, ACL2, unification algorithm |
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
44 | 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 |
|
42 | Panagiotis Manolios, Daron Vroon 0001 |
Algorithms for Ordinal Arithmetic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings, pp. 243-257, 2003, Springer, 3-540-40559-3. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
42 | Jun Sawada, Ruben Gamboa |
Mechanical Verification of a Square Root Algorithm Using Taylor's Theorem. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMCAD ![In: Formal Methods in Computer-Aided Design, 4th International Conference, FMCAD 2002, Portland, OR, USA, November 6-8, 2002, Proceedings, pp. 274-291, 2002, Springer, 3-540-00116-6. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
42 | William McCune, Olga Shumsky |
System Description: IVY. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-17, 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings, pp. 401-405, 2000, Springer, 3-540-67664-3. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
35 | Francisco-Jesús Martín-Mateos, Julio Rubio 0001, José-Luis Ruiz-Reina |
ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Calculemus/MKM ![In: Intelligent Computer Mathematics, 16th Symposium, Calculemus 2009, 8th International Conference, MKM 2009, Held as Part of CICM 2009, Grand Bend, Canada, July 6-12, 2009. Proceedings, pp. 106-121, 2009, Springer, 978-3-642-02613-3. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
35 | J Strother Moore, Qiang Zhang |
Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, pp. 373-384, 2005, Springer, 3-540-28372-2. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
35 | Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo |
Proof Pearl: A Formal Proof of Higman's Lemma in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, pp. 358-372, 2005, Springer, 3-540-28372-2. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
35 | Hanbing Liu, J Strother Moore |
Java Program Verification via a JVM Deep Embedding in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings, pp. 184-200, 2004, Springer, 3-540-23017-3. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
35 | Inmaculada Medina-Bulo, Francisco Palomo-Lozano, José A. Alonso-Jiménez, José-Luis Ruiz-Reina |
Verified Computer Algebra in Acl2. Gröbner Bases Computation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AISC ![In: Artificial Intelligence and Symbolic Computation, 7th International Conference, AISC 2004, Linz, Austria, September 22-24, 2004, Proceedings, pp. 171-184, 2004, Springer, 3-540-23212-5. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
35 | Ghiath Al Sammane, Diana Toma, Julien Schmaltz, Pierre Ostier, Dominique Borrione |
Constrained Symbolic Simulation with Mathematica and ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CHARME ![In: Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003, Proceedings, pp. 150-157, 2003, Springer, 3-540-20363-X. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
35 | J Strother Moore |
An ACL2 Proof of Write Invalidate Cache Coherence. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV ![In: Computer Aided Verification, 10th International Conference, CAV '98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings, pp. 29-38, 1998, Springer, 3-540-64608-6. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
35 | J Strother Moore |
Symbolic Simulation: An ACL2 Approach. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMCAD ![In: Formal Methods in Computer-Aided Design, Second International Conference, FMCAD '98, Palo Alto, California, USA, November 4-6, 1998, Proceedings, pp. 334-350, 1998, Springer, 3-540-65191-8. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
35 | William D. Young |
Comparing Verification Systems: Interactive Consistency in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 23(4), pp. 214-223, 1997. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
fault tolerance, Formal verification, specification languages, computational logic, automatic theorem proving |
28 | Sandip Ray, Warren A. Hunt Jr., John Matthews, J Strother Moore |
A Mechanical Analysis of Program Verification Strategies. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 40(4), pp. 245-269, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
Inductive assertions, Partial correctness, Theorem proving, Invariants, Total correctness |
28 | Dominique Borrione, Amr Helmy, Laurence V. Pierre, Julien Schmaltz |
A Generic Model for Formally Verifying NoC Communication Architectures: A Case Study. ![Search on Bibsonomy](Pics/bibsonomy.png) |
NOCS ![In: First International Symposium on Networks-on-Chips, NOCS 2007, 7-9 May 2007, Princeton, New Jersey, USA, Proceedings, pp. 127-136, 2007, IEEE Computer Society, 978-0-7695-2773-4. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
28 | David M. Russinoff |
A Mathematical Approach to RTL Verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV ![In: Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings, pp. 2, 2007, Springer, 978-3-540-73367-6. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
28 | Matt Kaufmann, Konrad Slind |
Proof Pearl: Wellfounded Induction on the Ordinals Up to epsilon 0. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings, pp. 294-301, 2007, Springer, 978-3-540-74590-7. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
28 | Panagiotis Manolios, Daron Vroon 0001 |
Termination Analysis with Calling Context Graphs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV ![In: Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, pp. 401-414, 2006, Springer, 3-540-37406-X. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
28 | Warren A. Hunt Jr., Erik Reeber |
Formalization of the DE2 Language. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CHARME ![In: Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2005, Saarbrücken, Germany, October 3-6, 2005, Proceedings, pp. 20-34, 2005, Springer, 3-540-29105-9. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
28 | Sandip Ray, J Strother Moore |
Proof Styles in Operational Semantics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMCAD ![In: Formal Methods in Computer-Aided Design, 5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings, pp. 67-81, 2004, Springer, 3-540-23738-0. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
28 | Julien Schmaltz, Dominique Borrione |
A Functional Approach to the Formal Specification of Networks on Chip. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMCAD ![In: Formal Methods in Computer-Aided Design, 5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings, pp. 52-66, 2004, Springer, 3-540-23738-0. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
28 | J Strother Moore, George Porter |
The apprentice challenge. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Program. Lang. Syst. ![In: ACM Trans. Program. Lang. Syst. 24(3), pp. 193-216, 2002. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
Java, theorem proving, Java Virtual Machine, mutual exclusion, operational semantics, parallel and distributed computation |
28 | Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo, José-Luis Ruiz-Reina |
Verifying an Applicative ATP Using Multiset Relations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
EUROCAST ![In: Computer Aided Systems Theory - EUROCAST 2001, Las Palmas de Gran Canaria, Spain, February 19-23, 2001, Revised Papers, pp. 612-626, 2001, Springer, 3-540-42959-X. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
28 | Jun Sawada, Warren A. Hunt Jr. |
Hardware Modeling Using Function Encapsulation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMCAD ![In: Formal Methods in Computer-Aided Design, Third International Conference, FMCAD 2000, Austin, Texas, USA, November 1-3, 2000, Proceedings, pp. 234-245, 2000, Springer, 3-540-41219-0. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
28 | Matt Kaufmann, J Strother Moore |
An Industrial Strength Theorem Prover for a Logic Based on Common Lisp. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 23(4), pp. 203-213, 1997. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
total functions, microcode verification, floating point division, Formal verification, digital signal processing, type checking, computational logic, automatic theorem proving, partial functions |
22 | Jagadish Bapanapally, Ruben Gamboa |
A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 5:1-5:15, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
22 | Jagadish Bapanapally, Ruben Gamboa |
A Formal Proof of the Banach-Tarski Theorem in ACL2(r). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISAIM ![In: Proceedings of the International Symposium on Artificial Intelligence and Mathematics 2022 (ISAIM 2022), Fort Lauderdale, Florida, USA, January 3-5, 2022, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP BibTeX RDF |
|
22 | Mahum Naseer, Waqar Ahmad, Osman Hasan |
Formal Verification of ECCs for Memories Using ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Electron. Test. ![In: J. Electron. Test. 36(5), pp. 643-663, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
22 | J Strother Moore |
Milestones from the Pure Lisp theorem prover to ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 31(6), pp. 699-732, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
22 | Yan Peng, Mark R. Greenstreet |
Verifying Timed, Asynchronous Circuits using ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ASYNC ![In: 25th IEEE International Symposium on Asynchronous Circuits and Systems, ASYNC 2019, Hirosaki, Japan, May 12-15, 2019, pp. 96-104, 2019, IEEE, 978-1-5386-4747-9. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
22 | Mihir Parang Mehta, William R. Cook |
Binary-Compatible Verification of Filesystems with ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 25:1-25:18, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
22 | J Strother Moore, Marijn J. H. Heule |
Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ARCADE@CADE ![In: ARCADE 2017, 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, Gothenburg, Sweden, 6th August 2017, pp. 42-45, 2017, EasyChair. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
22 | Cuong K. Chau, Warren A. Hunt Jr., Marly Roncken, Ivan E. Sutherland |
A Framework for Asynchronous Circuit Modeling and Verification in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Haifa Verification Conference ![In: Hardware and Software: Verification and Testing - 13th International Haifa Verification Conference, HVC 2017, Haifa, Israel, November 13-15, 2017, Proceedings, pp. 3-18, 2017, Springer, 978-3-319-70388-6. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
22 | Laureano Lambán, Francisco J. Martín-Mateos, Julio Rubio 0001, José-Luis Ruiz-Reina |
Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings, pp. 354-370, 2017, Springer, 978-3-319-66106-3. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
22 | Jónathan Heras, Francisco-Jesús Martín-Mateos, Vico Pascual |
Modelling algebraic structures and morphisms in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Appl. Algebra Eng. Commun. Comput. ![In: Appl. Algebra Eng. Commun. Comput. 26(3), pp. 277-303, 2015. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
22 | Eric Smith, Alessandro Coglio |
Android Platform Modeling and Android App Verification in the ACL2 Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
VSTTE ![In: Verified Software: Theories, Tools, and Experiments - 7th International Conference, VSTTE 2015, San Francisco, CA, USA, July 18-19, 2015. Revised Selected Papers, pp. 183-201, 2015, Springer, 978-3-319-29612-8. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
22 | Jesús Aransay-Azofra, Jose Divasón, Jónathan Heras, Laureano Lambán, María Vico Pascual, Ángel Luis Rubio, Julio Rubio 0001 |
Obtaining an ACL2 Specification from an Isabelle/HOL Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AISC ![In: Artificial Intelligence and Symbolic Computation - 12th International Conference, AISC 2014, Seville, Spain, December 11-13, 2014. Proceedings, pp. 49-63, 2014, Springer, 978-3-319-13769-8. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
22 | Jónathan Heras, Ekaterina Komendantskaya, Moa Johansson, Ewen Maclean |
Proof-Pattern Recognition in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1308.1780, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP BibTeX RDF |
|
22 | Jónathan Heras, Ekaterina Komendantskaya, Moa Johansson, Ewen Maclean |
Proof-Pattern Recognition and Lemma Discovery in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings, pp. 389-406, 2013, Springer, 978-3-642-45220-8. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
22 | David S. Hardin |
The Specification, Verification, and Implementation of a High-Assurance Data Structure: An ACL2 Approach. ![Search on Bibsonomy](Pics/bibsonomy.png) |
HICSS ![In: 46th Hawaii International Conference on System Sciences, HICSS 2013, Wailea, HI, USA, January 7-10, 2013, pp. 5059-5067, 2013, IEEE Computer Society, 978-1-4673-5933-7. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
22 | Kevin Krause, Jim Alves-Foss |
On Designing an ACL2-Based C Integer Type Safety Checking Tool. ![Search on Bibsonomy](Pics/bibsonomy.png) |
NASA Formal Methods ![In: NASA Formal Methods, 5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings, pp. 472-477, 2013, Springer, 978-3-642-38087-7. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
22 | Michael J. C. Gordon, Matt Kaufmann, Sandip Ray |
The Right Tools for the Job: Correctness of Cone of Influence Reduction Proved Using ACL2 and HOL4. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 47(1), pp. 1-16, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
22 | Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo |
Proof Pearl: a Formal Proof of Higman's Lemma in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 47(3), pp. 229-250, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
22 | J Strother Moore |
Reasoning about digital artifacts with ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PLPV ![In: Proceedings of the 5th ACM Workshop Programming Languages meets Program Verification, PLPV 2011, Austin, TX, USA, January 29, 2011, pp. 1-2, 2011, ACM, 978-1-4503-0487-0. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
22 | Harsh Raju Chamarthi, Peter C. Dillinger, Panagiotis Manolios, Daron Vroon 0001 |
The ACL2 Sedan Theorem Proving System. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TACAS ![In: Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, pp. 291-295, 2011, Springer, 978-3-642-19834-2. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
22 | Laureano Lambán, Francisco-Jesús Martín-Mateos, Julio Rubio 0001, José-Luis Ruiz-Reina |
Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings, pp. 200-215, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
22 | Peter Reid, Ruben Gamboa |
Automatic Differentiation in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings, pp. 312-324, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|