Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
192 | Ruben Gamboa, John R. Cowles |
Implementing a cost-aware evaluator for ACL2 expressions. ![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. 71-80, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
ACL2 evaluator, function cost, evaluators |
178 | Warren A. Hunt Jr., Erik Reeber |
A SAT-based procedure for verifying finite state machines in 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. 127-135, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
satisfiability solving, theorem proving, hardware verification, ACL2 |
172 | Robert S. Boyer, Warren A. Hunt Jr. |
Function memoization and unique object representation for ACL2 functions. ![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. 81-89, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
ACL2 workshop, function memoization, hash CONS, hash CONSing, Lisp, ACL2 |
164 | Dale Vaillancourt, Rex L. Page, Matthias Felleisen |
ACL2 in DrScheme. ![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. 107-116, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
DrScheme, TeachScheme!, formal methods, pedagogy, ACL2 |
143 | Julien Schmaltz, Dominique Borrione |
Towards a formal theory of on chip communications in the ACL2 logic. ![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. 47-56, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
formal theory, network on a chip, theorem proving, communication theory |
143 | Lee Pike, Mark Shields, John Matthews |
A verifying core for a cryptographic language compiler. ![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. 1-10, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
cryptography, certification, optimizing compiler, ACL2, high-assurance, certifying compiler, verifying compiler |
136 | 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 |
136 | Jared Davis |
Reasoning about ACL2 file input. ![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. 117-126, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
UTF-8, file input, ACL2, unicode, exhaustive testing |
136 | Sol Swords, William R. Cook |
Soundness of the simply typed lambda calculus in 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. 35-39, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
lambda-calculus, soundness, ACL2 |
136 | Michael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds |
An embedding of the ACL2 logic in HOL. ![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. 40-46, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
HOL4, proof oracle, sound translation, verification, formal methods, logic, first-order logic, higher-order logic, ACL2, HOL |
132 | Michael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann |
An Integration of HOL and ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMCAD ![In: Formal Methods in Computer-Aided Design, 6th International Conference, FMCAD 2006, San Jose, California, USA, November 12-16, 2006, Proceedings, pp. 153-160, 2006, IEEE Computer Society, 0-7695-2707-8. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
129 | Matt Kaufmann, J Strother Moore |
Double rewriting for equivalential reasoning in 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. 103-106, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
double-rewrite, verification, formal methods, rewriting, congruences, equivalence relations |
129 | David A. Greve |
Parameterized congruences in 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. 28-34, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
123 | Jared Davis |
Memories: array-like records for 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. 57-60, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
MBE, fixnum optimization, linear address spaces, arrays, records, ACL2 |
123 | John R. Cowles, Ruben Gamboa |
Unique factorization in ACL2: Euclidean domains. ![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. 21-27, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
Boyer-Moore logic, Euclidean domains, unique factorization, ACL2 |
119 | Warren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J Strother Moore, Eric Whitman Smith |
Meta Reasoning 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. 163-178, 2005, Springer, 3-540-28372-2. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
115 | Erik Reeber, Jun Sawada |
Combining ACL2 and an automated verification tool to verify a multiplier. ![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. 63-70, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
model checking, theorem proving, hardware verification |
115 | David S. Hardin, Eric W. Smith, William D. Young |
A robust machine code proof framework for highly secure applications. ![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. 11-20, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
cryptography, theorem proving, certification, symbolic simulation, ACL2, high-assurance, processor modeling |
112 | Carl Eastlund, Matthias Felleisen |
Making induction manifest in modular ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PPDP ![In: Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, September 7-9, 2009, Coimbra, Portugal, pp. 105-116, 2009, ACM, 978-1-60558-568-0. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
theorem provers, acl2, module systems |
109 | 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 |
|
109 | 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 |
|
109 | Warren A. Hunt Jr., Serita M. Nelesen |
Phylogenetic trees in 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. 99-102, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
ACL2, phylogenetics |
105 | Peter C. Dillinger, Panagiotis Manolios, Daron Vroon 0001, J Strother Moore |
ACL2s: "The ACL2 Sedan". ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICSE Companion ![In: 29th International Conference on Software Engineering (ICSE 2007), Minneapolis, MN, USA, May 20-26, 2007, Companion Volume, pp. 59-60, 2007, IEEE Computer Society. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
105 | Warren A. Hunt Jr., Robert Bellarmine Krug, J Strother Moore |
Linear and Nonlinear Arithmetic in 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. 319-333, 2003, Springer, 3-540-20363-X. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
101 | Sandip Ray |
Quantification in tail-recursive function definitions. ![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. 95-98, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
formal methods, logic, ACL2, conservativity, skolemization |
91 | Carl Eastlund, Matthias Felleisen |
Toward a Practical Module System for ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PADL ![In: Practical Aspects of Declarative Languages, 11th International Symposium, PADL 2009, Savannah, GA, USA, January 19-20, 2009. Proceedings, pp. 46-60, 2009, Springer, 978-3-540-92994-9. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
91 | Erik Reeber, Warren A. Hunt Jr. |
A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA). ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, pp. 453-467, 2006, Springer, 3-540-37187-7. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
87 | 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 |
|
87 | 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 |
|
87 | 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 |
|
87 | 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 |
|
87 | 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 |
|
87 | 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 |
|
87 | 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 |
|
87 | 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 |
|
87 | 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 |
|
87 | 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 |
|
79 | Tony Hoare |
The ideal of verified software. ![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. 61-62, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
77 | Ruben Gamboa, John R. Cowles |
Theory Extension in ACL2(r). ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 38(4), pp. 273-301, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
Mathematics Subject Classifications (2000) 68T15, 03B35, 03H15 |
77 | J Strother Moore |
Finite Set Theory in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings, pp. 313-328, 2001, Springer, 3-540-42525-X. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
77 | Panagiotis Manolios, Sudarshan K. Srinivasan |
A Framework for Verifying Bit-Level Pipelined Machines Based on Automated Deduction and Decision Procedures. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 37(1-2), pp. 93-116, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
pipelined machines, bit-level, verification, refinement, automated reasoning, ACL2 |
77 | Panagiotis Manolios, Daron Vroon 0001 |
Ordinal Arithmetic: Algorithms and Mechanization. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 34(4), pp. 387-423, 2005. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
automated reasoning, arithmetic, ACL2, ordinal |
71 | Panagiotis Manolios, J Strother Moore |
Partial Functions in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 31(2), pp. 107-127, 2003. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
ACL2, partial functions |
69 | Jun Sawada, Erik Reeber |
ACL2SIX: A Hint used to Integrate a Theorem Prover and an Automated Verification Tool. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMCAD ![In: Formal Methods in Computer-Aided Design, 6th International Conference, FMCAD 2006, San Jose, California, USA, November 12-16, 2006, Proceedings, pp. 161-170, 2006, IEEE Computer Society, 0-7695-2707-8. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
69 | J Strother Moore |
Functional formal methods. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP ![In: Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002., pp. 123, 2002, ACM, 1-58113-487-8. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
functional programming, Java Virtual Machine, microarchitecture, software verification, Common Lisp, hardware verification, mechanical theorem proving |
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | 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 |
|
66 | Panagiotis Manolios, Matthew Wilding (eds.) |
Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006 ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![ACM, 0-9788493-0-2 The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP BibTeX RDF |
|
63 | Matt Kaufmann, J Strother Moore |
An ACL2 Tutorial. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, pp. 17-21, 2008, Springer, 978-3-540-71065-3. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
63 | Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo, José-Luis Ruiz-Reina |
A Formal Proof of Dickson's Lemma in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic for Programming, Artificial Intelligence, and Reasoning, 10th International Conference, LPAR 2003, Almaty, Kazakhstan, September 22-26, 2003, Proceedings, pp. 49-58, 2003, Springer, 3-540-20101-7. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
63 | Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo, José-Luis Ruiz-Reina |
Formal Verification of Molecular Computational Models in ACL2: A Case Study. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAEPIA ![In: Current Topics in Artificial Intelligence, 10th Conference of the Spanish Association for Artificial Intelligence, CAEPIA 2003, and 5th Conference on Technology Transfer, TTIA 2003, San Sebastian, Spain, November 12-14, 2003. Revised Selected Papers, pp. 344-353, 2003, Springer, 3-540-22218-9. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
63 | José-Luis Ruiz-Reina, José Antonio Alonso Jimenez, María-José Hidalgo, Francisco-Jesús Martín-Mateos |
Formal Reasoning about Efficient Data Structures: A Case Study in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LOPSTR ![In: Logic Based Program Synthesis and Transformation, 13th International Symposium LOPSTR 2003, Uppsala, Sweden, August 25-27, 2003, Revised Selected Papers, pp. 75-91, 2003, Springer, 3-540-22174-3. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
63 | Robert S. Boyer, J Strother Moore |
Single-Threaded Objects in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PADL ![In: Practical Aspects of Declarative Languages, 4th International Symposium, PADL 2002, Portland, OR, USA, January 19-20, 2002, Proceedings, pp. 9-27, 2002, Springer, 3-540-43092-X. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
63 | Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo, José-Luis Ruiz-Reina |
Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LOPSTR ![In: Logic Based Program Synthesis and Tranformation, 12th International Workshop, LOPSTR 2002, Madrid, Spain, September 17-20,2002, Revised Selected Papers, pp. 182-198, 2002, Springer, 3-540-40438-4. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
63 | José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo, Francisco-Jesús Martín-Mateos |
Formalizing Rewriting in the ACL2 Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AISC ![In: Artificial Intelligence and Symbolic Computation, International Conference AISC 2000 Madrid, Spain, July 17-19, 2000, Revised Papers, pp. 92-106, 2000, Springer, 3-540-42071-1. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|