Search results for "acl2"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
57	Ruben A. Gamboa	A Formalization of Powerlist Algebra in ACL2.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF	Powerlists, Verification, ACL2
57	Matt Kaufmann	Verification of Year 2000 conversion rules using the ACL2 theorem prover.	Int. J. Softw. Tools Technol. Transf.	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.	CAV	2009	DBLP DOI BibTeX RDF
49	Bishop Brock, Matt Kaufmann, J Strother Moore	Rewriting with Equivalence Relations in ACL2.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Refinement, Rewriting, Congruence, Equivalence relations
49	James Reynolds	Automatically Translating Type and Function Definitions from HOL to ACL2.	TPHOLs	2007	DBLP DOI BibTeX RDF
49	Mirian Andrés, Laureano Lambán, Julio Rubio 0001	Executing in Common Lisp, Proving in ACL2.	Calculemus/MKM	2007	DBLP DOI BibTeX RDF
49	Diana Toma, Dominique Borrione	Formal Verification of a SHA-1 Circuit Core Using ACL2.	TPHOLs	2005	DBLP DOI BibTeX RDF
49	Yann Zimmermann, Diana Toma	Component Reuse in B Using ACL2.	ZB	2005	DBLP DOI BibTeX RDF
49	Panagiotis Manolios, Daron Vroon 0001	Integrating Reasoning About Ordinal Arithmetic into ACL2.	FMCAD	2004	DBLP DOI BibTeX RDF
49	Magali Contensin, Laurence Pierre	Combining ACL2 and a v-calculus Model-Checker to Verify System-Level Designs.	MEMOCODE	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.	FMCAD	2000	DBLP DOI BibTeX RDF
49	Matt Kaufmann	ACL2 Support for Verification Projects (Invited Talk).	CADE	1998	DBLP DOI BibTeX RDF
49	Sandip Ray, Rob Sumners	Combining Theorem Proving with Model Checking through Predicate Abstraction.	IEEE Des. Test Comput.	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.	J. Autom. Reason.	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.	ACL2	2023	DBLP DOI BibTeX RDF
44	Andrew T. Walter, Ankit Kumar, Panagiotis Manolios	Proving Calculational Proofs Correct.	ACL2	2023	DBLP DOI BibTeX RDF
44	Alessandro Coglio, Eric McCarthy, Eric W. Smith	Formal Verification of Zero-Knowledge Circuits.	ACL2	2023	DBLP DOI BibTeX RDF
44	David M. Russinoff	A Formalization of Finite Group Theory: Part III.	ACL2	2023	DBLP DOI BibTeX RDF
44	David M. Russinoff	A Formalization of Finite Group Theory: Part II.	ACL2	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.	ACL2	2023	DBLP DOI BibTeX RDF
44	Ankit Kumar, Max von Hippel, Panagiotis Manolios, Cristina Nita-Rotaru	Verification of GossipSub in ACL2s.	ACL2	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.	ACL2	2022	DBLP DOI BibTeX RDF
44	Ruben Gamboa, Woodrow Gamboa	All Prime Numbers Have Primitive Roots.	ACL2	2022	DBLP DOI BibTeX RDF
44	Jagadish Bapanapally, Ruben Gamboa	A Free Group of Rotations of Rank 2.	ACL2	2022	DBLP DOI BibTeX RDF
44	David M. Russinoff	Properties of the Hebrew Calendar.	ACL2	2022	DBLP DOI BibTeX RDF
44	Warren A. Hunt Jr., Vivek Ramanathan, J Strother Moore	VWSIM: A Circuit Simulator.	ACL2	2022	DBLP DOI BibTeX RDF
44	Andrew T. Walter, Panagiotis Manolios	ACL2s Systems Programming.	ACL2	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.	ACL2	2022	DBLP DOI BibTeX RDF
44	David M. Russinoff	A Formalization of Finite Group Theory.	ACL2	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.	ACL2	2020	DBLP DOI BibTeX RDF
44	Rob Sumners	Computing and Proving Well-founded Orderings through Finite Abstractions.	ACL2	2020	DBLP DOI BibTeX RDF
44	Sol Swords	New Rewriter Features in FGL.	ACL2	2020	DBLP DOI BibTeX RDF
44	Sol Swords	Generating Mutually Inductive Theorems from Concise Descriptions.	ACL2	2020	DBLP DOI BibTeX RDF
44	Alessandro Coglio, Stephen J. Westfold	Isomorphic Data Type Transformations.	ACL2	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.	ACL2	2018	DBLP DOI BibTeX RDF
44	David A. Greve, Andrew Gacek	Trapezoidal Generalization over Linear Constraints.	ACL2	2018	DBLP DOI BibTeX RDF
44	Matt Kaufmann	DefunT: A Tool for Automating Termination Proofs by Using the Community Books (Extended Abstract).	ACL2	2018	DBLP DOI BibTeX RDF
44	Yan Peng, Mark R. Greenstreet	Smtlink 2.0.	ACL2	2018	DBLP DOI BibTeX RDF
44	Sol Swords	Incremental SAT Library Integration Using Abstract Stobjs.	ACL2	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.	ACL2	2017	DBLP BibTeX RDF
44	Rob Sumners	Proof Reduction of Fair Stuttering Refinement of Asynchronous Systems and Applications.	ACL2	2017	DBLP DOI BibTeX RDF
44	Sol Swords	Term-Level Reasoning in Support of Bit-blasting.	ACL2	2017	DBLP DOI BibTeX RDF
44	Matt Kaufmann, Sol Swords	Meta-extract: Using Existing Facts in Meta-reasoning.	ACL2	2017	DBLP DOI BibTeX RDF
44	David M. Russinoff	A Computationally Surveyable Proof of the Group Properties of an Elliptic Curve.	ACL2	2017	DBLP DOI BibTeX RDF
44	Alessandro Coglio, Matt Kaufmann, Eric Whitman Smith	A Versatile, Sound Tool for Simplifying Definitions.	ACL2	2017	DBLP DOI BibTeX RDF
44	Shilpi Goel	The x86isa Books: Features, Usage, and Future Plans.	ACL2	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.	ACL2	2015	DBLP DOI BibTeX RDF
44	David S. Hardin	Reasoning About LLVM Code Using Codewalker.	ACL2	2015	DBLP DOI BibTeX RDF
44	J Strother Moore	Stateman: Using Metafunctions to Manage Large Terms Representing Machine States.	ACL2	2015	DBLP DOI BibTeX RDF
44	Mitesh Jain, Panagiotis Manolios	Proving Skipping Refinement with ACL2s.	ACL2	2015	DBLP DOI BibTeX RDF
44	Sol Swords, Jared Davis	Fix Your Types.	ACL2	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.	ACL2	2014	DBLP DOI BibTeX RDF
44	Ruben Gamboa, John R. Cowles	Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent.	ACL2	2014	DBLP DOI BibTeX RDF
44	John R. Cowles, Ruben Gamboa	Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis.	ACL2	2014	DBLP DOI BibTeX RDF
42	Panagiotis Manolios, Daron Vroon 0001	Algorithms for Ordinal Arithmetic.	CADE	2003	DBLP DOI BibTeX RDF
42	Jun Sawada, Ruben Gamboa	Mechanical Verification of a Square Root Algorithm Using Taylor's Theorem.	FMCAD	2002	DBLP DOI BibTeX RDF
42	William McCune, Olga Shumsky	System Description: IVY.	CADE	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.	Calculemus/MKM	2009	DBLP DOI BibTeX RDF
35	J Strother Moore, Qiang Zhang	Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2.	TPHOLs	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.	TPHOLs	2005	DBLP DOI BibTeX RDF
35	Hanbing Liu, J Strother Moore	Java Program Verification via a JVM Deep Embedding in ACL2.	TPHOLs	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.	AISC	2004	DBLP DOI BibTeX RDF
35	Ghiath Al Sammane, Diana Toma, Julien Schmaltz, Pierre Ostier, Dominique Borrione	Constrained Symbolic Simulation with Mathematica and ACL2.	CHARME	2003	DBLP DOI BibTeX RDF
35	J Strother Moore	An ACL2 Proof of Write Invalidate Cache Coherence.	CAV	1998	DBLP DOI BibTeX RDF
35	J Strother Moore	Symbolic Simulation: An ACL2 Approach.	FMCAD	1998	DBLP DOI BibTeX RDF
35	William D. Young	Comparing Verification Systems: Interactive Consistency in ACL2.	IEEE Trans. Software Eng.	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.	J. Autom. Reason.	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.	NOCS	2007	DBLP DOI BibTeX RDF
28	David M. Russinoff	A Mathematical Approach to RTL Verification.	CAV	2007	DBLP DOI BibTeX RDF
28	Matt Kaufmann, Konrad Slind	Proof Pearl: Wellfounded Induction on the Ordinals Up to epsilon 0.	TPHOLs	2007	DBLP DOI BibTeX RDF
28	Panagiotis Manolios, Daron Vroon 0001	Termination Analysis with Calling Context Graphs.	CAV	2006	DBLP DOI BibTeX RDF
28	Warren A. Hunt Jr., Erik Reeber	Formalization of the DE2 Language.	CHARME	2005	DBLP DOI BibTeX RDF
28	Sandip Ray, J Strother Moore	Proof Styles in Operational Semantics.	FMCAD	2004	DBLP DOI BibTeX RDF
28	Julien Schmaltz, Dominique Borrione	A Functional Approach to the Formal Specification of Networks on Chip.	FMCAD	2004	DBLP DOI BibTeX RDF
28	J Strother Moore, George Porter	The apprentice challenge.	ACM Trans. Program. Lang. Syst.	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.	EUROCAST	2001	DBLP DOI BibTeX RDF
28	Jun Sawada, Warren A. Hunt Jr.	Hardware Modeling Using Function Encapsulation.	FMCAD	2000	DBLP DOI BibTeX RDF
28	Matt Kaufmann, J Strother Moore	An Industrial Strength Theorem Prover for a Logic Based on Common Lisp.	IEEE Trans. Software Eng.	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).	ITP	2022	DBLP DOI BibTeX RDF
22	Jagadish Bapanapally, Ruben Gamboa	A Formal Proof of the Banach-Tarski Theorem in ACL2(r).	ISAIM	2022	DBLP BibTeX RDF
22	Mahum Naseer, Waqar Ahmad, Osman Hasan	Formal Verification of ECCs for Memories Using ACL2.	J. Electron. Test.	2020	DBLP DOI BibTeX RDF
22	J Strother Moore	Milestones from the Pure Lisp theorem prover to ACL2.	Formal Aspects Comput.	2019	DBLP DOI BibTeX RDF
22	Yan Peng, Mark R. Greenstreet	Verifying Timed, Asynchronous Circuits using ACL2.	ASYNC	2019	DBLP DOI BibTeX RDF
22	Mihir Parang Mehta, William R. Cook	Binary-Compatible Verification of Filesystems with ACL2.	ITP	2019	DBLP DOI BibTeX RDF
22	J Strother Moore, Marijn J. H. Heule	Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions.	ARCADE@CADE	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.	Haifa Verification Conference	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.	ITP	2017	DBLP DOI BibTeX RDF
22	Jónathan Heras, Francisco-Jesús Martín-Mateos, Vico Pascual	Modelling algebraic structures and morphisms in ACL2.	Appl. Algebra Eng. Commun. Comput.	2015	DBLP DOI BibTeX RDF
22	Eric Smith, Alessandro Coglio	Android Platform Modeling and Android App Verification in the ACL2 Theorem Prover.	VSTTE	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.	AISC	2014	DBLP DOI BibTeX RDF
22	Jónathan Heras, Ekaterina Komendantskaya, Moa Johansson, Ewen Maclean	Proof-Pattern Recognition in ACL2.	CoRR	2013	DBLP BibTeX RDF
22	Jónathan Heras, Ekaterina Komendantskaya, Moa Johansson, Ewen Maclean	Proof-Pattern Recognition and Lemma Discovery in ACL2.	LPAR	2013	DBLP DOI BibTeX RDF
22	David S. Hardin	The Specification, Verification, and Implementation of a High-Assurance Data Structure: An ACL2 Approach.	HICSS	2013	DBLP DOI BibTeX RDF
22	Kevin Krause, Jim Alves-Foss	On Designing an ACL2-Based C Integer Type Safety Checking Tool.	NASA Formal Methods	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.	J. Autom. Reason.	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.	J. Autom. Reason.	2011	DBLP DOI BibTeX RDF
22	J Strother Moore	Reasoning about digital artifacts with ACL2.	PLPV	2011	DBLP DOI BibTeX RDF
22	Harsh Raju Chamarthi, Peter C. Dillinger, Panagiotis Manolios, Daron Vroon 0001	The ACL2 Sedan Theorem Proving System.	TACAS	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.	ITP	2011	DBLP DOI BibTeX RDF
22	Peter Reid, Ruben Gamboa	Automatic Differentiation in ACL2.	ITP	2011	DBLP DOI BibTeX RDF