Search results for "ACL2"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
192	Ruben Gamboa, John R. Cowles	Implementing a cost-aware evaluator for ACL2 expressions.	ACL2	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.	ACL2	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.	ACL2	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.	ACL2	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.	ACL2	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.	ACL2	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.	ACL2	2006	DBLP DOI BibTeX RDF	pand, parallel ACL2, pcall, plet, por, granularity, functional language
136	Jared Davis	Reasoning about ACL2 file input.	ACL2	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.	ACL2	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.	ACL2	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.	FMCAD	2006	DBLP DOI BibTeX RDF
129	Matt Kaufmann, J Strother Moore	Double rewriting for equivalential reasoning in ACL2.	ACL2	2006	DBLP DOI BibTeX RDF	double-rewrite, verification, formal methods, rewriting, congruences, equivalence relations
129	David A. Greve	Parameterized congruences in ACL2.	ACL2	2006	DBLP DOI BibTeX RDF
123	Jared Davis	Memories: array-like records for ACL2.	ACL2	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.	ACL2	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.	TPHOLs	2005	DBLP DOI BibTeX RDF
115	Erik Reeber, Jun Sawada	Combining ACL2 and an automated verification tool to verify a multiplier.	ACL2	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.	ACL2	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.	PPDP	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	ACL2	2013	DBLP DOI BibTeX RDF
109	Matt Kaufmann, J Strother Moore	How Can I Do That with ACL2? Recent Enhancements to ACL2	ACL2	2011	DBLP DOI BibTeX RDF
109	Warren A. Hunt Jr., Serita M. Nelesen	Phylogenetic trees in ACL2.	ACL2	2006	DBLP DOI BibTeX RDF	ACL2, phylogenetics
105	Peter C. Dillinger, Panagiotis Manolios, Daron Vroon 0001, J Strother Moore	ACL2s: "The ACL2 Sedan".	ICSE Companion	2007	DBLP DOI BibTeX RDF
105	Warren A. Hunt Jr., Robert Bellarmine Krug, J Strother Moore	Linear and Nonlinear Arithmetic in ACL2.	CHARME	2003	DBLP DOI BibTeX RDF
101	Sandip Ray	Quantification in tail-recursive function definitions.	ACL2	2006	DBLP DOI BibTeX RDF	formal methods, logic, ACL2, conservativity, skolemization
91	Carl Eastlund, Matthias Felleisen	Toward a Practical Module System for ACL2.	PADL	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).	IJCAR	2006	DBLP DOI BibTeX RDF
87	Alessandro Coglio	A Complex Java Code Generator for ACL2 Based on a Shallow Embedding of ACL2 in Java.	ACL2	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.	ACL2	2022	DBLP DOI BibTeX RDF
87	Alessandro Coglio	A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java.	ACL2	2018	DBLP DOI BibTeX RDF
87	Jónathan Heras, Ekaterina Komendantskaya	ACL2(ml): Machine-Learning for ACL2.	ACL2	2014	DBLP DOI BibTeX RDF
87	Jared Davis, Sol Swords	Verified AIG Algorithms in ACL2	ACL2	2013	DBLP DOI BibTeX RDF
87	Matt Kaufmann, J Strother Moore	Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1	ACL2	2013	DBLP DOI BibTeX RDF
87	Caleb Eggensperger	Proof Pad: A New Development Environment for ACL2	ACL2	2013	DBLP DOI BibTeX RDF
87	Peter Reid, Ruben Gamboa	Implementing an Automatic Differentiator in ACL2	ACL2	2011	DBLP DOI BibTeX RDF
87	Sol Swords, Jared Davis	Bit-Blasting ACL2 Theorems	ACL2	2011	DBLP DOI BibTeX RDF
87	John R. Cowles, Ruben Gamboa	Verifying Sierpinski and Riesel Numbers in ACL2	ACL2	2011	DBLP DOI BibTeX RDF
79	Tony Hoare	The ideal of verified software.	ACL2	2006	DBLP DOI BibTeX RDF
77	Ruben Gamboa, John R. Cowles	Theory Extension in ACL2(r).	J. Autom. Reason.	2007	DBLP DOI BibTeX RDF	Mathematics Subject Classifications (2000) 68T15, 03B35, 03H15
77	J Strother Moore	Finite Set Theory in ACL2.	TPHOLs	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.	J. Autom. Reason.	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.	J. Autom. Reason.	2005	DBLP DOI BibTeX RDF	automated reasoning, arithmetic, ACL2, ordinal
71	Panagiotis Manolios, J Strother Moore	Partial Functions in ACL2.	J. Autom. Reason.	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.	FMCAD	2006	DBLP DOI BibTeX RDF
69	J Strother Moore	Functional formal methods.	ICFP	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.	ACL2	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.	ACL2	2023	DBLP DOI BibTeX RDF
66	Grant O. Passmore	ACL2 Proofs of Nonlinear Inequalities with Imandra.	ACL2	2023	DBLP DOI BibTeX RDF
66	David S. Hardin	Verification of a Rust Implementation of Knuth's Dancing Links using ACL2.	ACL2	2023	DBLP DOI BibTeX RDF
66	Mertcan Temel	Verified Implementation of an Efficient Term-Rewriting Algorithm for Multiplier Verification on ACL2.	ACL2	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.	ACL2	2022	DBLP DOI BibTeX RDF
66	Ruben Gamboa, Alicia Thoney	Using ACL2 To Teach Students About Software Testing.	ACL2	2022	DBLP DOI BibTeX RDF
66	David S. Hardin	Hardware/Software Co-Assurance using the Rust Programming Language and ACL2.	ACL2	2022	DBLP DOI BibTeX RDF
66	William D. Young	Modeling Asymptotic Complexity Using ACL2.	ACL2	2022	DBLP DOI BibTeX RDF
66	Alessandro Coglio	Ethereum's Recursive Length Prefix in ACL2.	ACL2	2020	DBLP DOI BibTeX RDF
66	Mertcan Temel	RP-Rewriter: An Optimized Rewriter for Large Terms in ACL2.	ACL2	2020	DBLP DOI BibTeX RDF
66	Ruben Gamboa, John R. Cowles, Woodrow Gamboa	Quadratic Extensions in ACL2.	ACL2	2020	DBLP DOI BibTeX RDF
66	David M. Russinoff	Formal Verification of Arithmetic RTL: Translating Verilog to C++ to ACL2.	ACL2	2020	DBLP DOI BibTeX RDF
66	Matt Kaufmann, J Strother Moore	Iteration in ACL2.	ACL2	2020	DBLP DOI BibTeX RDF
66	Carl Kwan, Mark R. Greenstreet	Real Vector Spaces and the Cauchy-Schwarz Inequality in ACL2(r).	ACL2	2018	DBLP DOI BibTeX RDF
66	Alessandro Coglio, Shilpi Goel	Adding 32-bit Mode to the ACL2 Model of the x86 ISA.	ACL2	2018	DBLP DOI BibTeX RDF
66	Carl Kwan, Mark R. Greenstreet	Convex Functions in ACL2(r).	ACL2	2018	DBLP DOI BibTeX RDF
66	Sol Swords	Hint Orchestration Using ACL2's Simplifier.	ACL2	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.	ACL2	2018	DBLP DOI BibTeX RDF
66	Ruben Gamboa, John R. Cowles	The Fundamental Theorem of Algebra in ACL2.	ACL2	2018	DBLP DOI BibTeX RDF
66	Mihir Parang Mehta	Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32.	ACL2	2018	DBLP DOI BibTeX RDF
66	John R. Cowles, Ruben Gamboa	The Cayley-Dickson Construction in ACL2.	ACL2	2017	DBLP DOI BibTeX RDF
66	John R. Cowles, Ruben Gamboa	Perfect Numbers in ACL2.	ACL2	2015	DBLP DOI BibTeX RDF
66	Cuong K. Chau, Matt Kaufmann, Warren A. Hunt Jr.	Fourier Series Formalization in ACL2(r).	ACL2	2015	DBLP DOI BibTeX RDF
66	Alessandro Coglio	Second-Order Functions and Theorems in ACL2.	ACL2	2015	DBLP DOI BibTeX RDF
66	Yan Peng, Mark R. Greenstreet	Extending ACL2 with SMT Solvers.	ACL2	2015	DBLP DOI BibTeX RDF
66	Disha Puri, Sandip Ray, Kecheng Hao, Fei Xie	Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis.	ACL2	2014	DBLP DOI BibTeX RDF
66	Matt Kaufmann, J Strother Moore	Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4.	ACL2	2014	DBLP DOI BibTeX RDF
66	Jared Davis, Matt Kaufmann	Industrial-Strength Documentation for ACL2.	ACL2	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.	ACL2	2014	DBLP DOI BibTeX RDF
66	Harsh Raju Chamarthi, Peter C. Dillinger, Panagiotis Manolios	Data Definitions in the ACL2 Sedan.	ACL2	2014	DBLP DOI BibTeX RDF
66	Benjamin Selfridge, Eric Smith	Polymorphic Types in ACL2.	ACL2	2014	DBLP DOI BibTeX RDF
66	Benjamin Selfridge	An ACL2 Mechanization of an Axiomatic Framework for Weak Memory.	ACL2	2014	DBLP DOI BibTeX RDF
66	John W. O'Leary, David M. Russinoff	Modeling Algorithms in SystemC and ACL2.	ACL2	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.	ACL2	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.	ACL2	2013	DBLP DOI BibTeX RDF
66	Bernard van Gastel, Julien Schmaltz	A formalisation of XMAS	ACL2	2013	DBLP DOI BibTeX RDF
66	David A. Greve, Konrad Slind	A Step-Indexing Approach to Partial Functions	ACL2	2013	DBLP DOI BibTeX RDF
66	Lucas Helms, Ruben Gamboa	An Interpreter for Quantum Circuits	ACL2	2013	DBLP DOI BibTeX RDF
66	Shilpi Goel, Warren A. Hunt Jr., Matt Kaufmann	Abstract Stobjs and Their Application to ISA Modeling	ACL2	2013	DBLP DOI BibTeX RDF
66	Sebastiaan J. C. Joosten, Bernard van Gastel, Julien Schmaltz	A Macro for Reusing Abstract Functions and Theorems	ACL2	2013	DBLP DOI BibTeX RDF
66	Freek Verbeek, Julien Schmaltz	Verification of Building Blocks for Asynchronous Circuits	ACL2	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.	ACL2	2011	DBLP DOI BibTeX RDF
66	Freek Verbeek, Julien Schmaltz	Formal verification of a deadlock detection algorithm	ACL2	2011	DBLP DOI BibTeX RDF
66	Peter-Michael Seidel	Formal Verification of an Iterative Low-Power x86 Floating-Point Multiplier with Redundant Feedback	ACL2	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	ACL2	2011	DBLP DOI BibTeX RDF
66	Harsh Raju Chamarthi, Peter C. Dillinger, Matt Kaufmann, Panagiotis Manolios	Integrating Testing and Interactive Theorem Proving	ACL2	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	ACL2	2006	DBLP BibTeX RDF
63	Matt Kaufmann, J Strother Moore	An ACL2 Tutorial.	TPHOLs	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.	LPAR	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.	CAEPIA	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.	LOPSTR	2003	DBLP DOI BibTeX RDF
63	Robert S. Boyer, J Strother Moore	Single-Threaded Objects in ACL2.	PADL	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.	LOPSTR	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.	AISC	2000	DBLP DOI BibTeX RDF