		Search-engine friendly clone of the ACL2 documentation.

Pubs-papers

Pubs-workshops

ACL2 Workshop Papers and Publications

This section contains documentation for papers and publications related to ACL2 workshops and conferences.

Total number of entries: 281

An Exercise in Graph Theory, J Strother Moore, in Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Publishers, 2000, June, pp. 41-74, ISBN: 0792378490. [Book Chapter]
Modular Proof: The Fundamental Theorem of Calculus, Matt Kaufmann, in Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Publishers, 2000, June, pp. 75-92, ISBN: 0792378490. [Book Chapter]
Mu-Calculus Model-Checking, Panagiotis Manolios, in Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Publishers, 2000, June, pp. 93-112, ISBN: 0792378490. [Book Chapter]
High-Speed, Analyzable Simulators, David Greve and Matthew Wilding and David Hardin, in Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Publishers, 2000, June, pp. 113-136, ISBN: 0792378490. [Book Chapter]
Verification of a Simple Pipelined Machine Model, Jun Sawada, in Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Publishers, 2000, June, pp. 137-150, ISBN: 0792378490. [Book Chapter]
The DE Language, Warren A. Hunt, Jr. , in Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Publishers, 2000, June, pp. 151-166, ISBN: 0792378490. [Book Chapter]
Using Macros to Mimic VHDL , Dominique Borrione and Philippe Georgelin and Vanderlei Rodrigues, in Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Publishers, 2000, June, pp. 167-184, ISBN: 0792378490. [Book Chapter]
Symbolic Trajectory Evaluation, Damir A. Jamsek, in Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Publishers, 2000, June, pp. 185-200, ISBN: 0792378490. [Book Chapter]
RTL Verification: A Floating-Point Multiplier, David M. Russinoff and Arthur Flatau, in Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Publishers, 2000, June, pp. 201-232, ISBN: 0792378490. [Book Chapter]
Design Verification of a Safety-Critical Embedded Verifier, Piergiorgio Bertoli and Paolo Traverso, in Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Publishers, 2000, June, pp. 233-246, ISBN: 0792378490. [Book Chapter]
Compiler Verification Revisited, Wolfgang Goerigk, in Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Publishers, 2000, June, pp. 247-264, ISBN: 0792378490. [Book Chapter]
Ivy : A Preprocessor and Proof Checker for First-Order Logic, William McCune and Olga Shumsky, in Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Publishers, 2000, June, pp. 265-282, ISBN: 0792378490. [Book Chapter]
Knuth 's Generalization of McCarthy 's 91 Function, John Cowles, in Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Publishers, 2000, June, pp. 283-300, ISBN: 0792378490. [Book Chapter]
Continuity and Differentiability, Ruben Gamboa, in Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Publishers, 2000, June, pp. 301-316, ISBN: 0792378490. [Book Chapter]
ACL2 for Parallel Systems Software: A Progress Report, Ewing Lusk and William McCune, 2000, November. [Technical Report]
Using a Single-Threaded Object to Speed a Verified Graph Pathfinder, Matthew Wilding, 2000, November. [Technical Report]
Correcness Proof of a BDD Manager in the Context of Satisfiability Checking, Rob Sumners, 2000, November. [Technical Report]
Developing a Framework for Simulation, Verification and Testing of SDL Specifications, Olga Shumsky and Lawrence J. Henschen, 2000, November. [Technical Report]
Verification of Pipelined Machines in ACL2 , Panagiotis Manolios, 2000, November. [Technical Report]
An Incremental Stuttering Refinement Proof of a Concurrent Program in ACL2 , Rob Sumners, 2000, November. [Technical Report]
Multiset Relations: A Tool for Proving Termination, J. L. Ruiz-Reina and J. A. Alonso and M. J. Hidalgo and F. J. Mart\'in, 2000, November. [Technical Report]
Proving Preservation of Partial Correctness with ACL2 : A Mechanical Compiler Source Level Correctness Proof, Wolfgang Goerigk, 2000, November. [Technical Report]
ACL2 Computed Hints: Extension and Practice, Jun Sawada, 2000, November. [Technical Report]
Automatic Verification of Polynomial Rings: Fundamental Properties in ACL2 , I. Medina-Bulo and J. A. Alonso-Jim\'enez and F. Palomo-Lozano, 2000, November. [Technical Report]
A Mechanical Proof of the Chinese Remainder Theorem, David M. Russinoff, 2000, November. [Technical Report]
Partial Functions in ACL2 , Panagiotis Manolios and J Strother Moore, 2000, November. [Technical Report]
Knuth's Generalization of Takeuchi's Tarai Function: Preliminary Report, Tom Bailey and John Cowles, 2000, November. [Technical Report]
Verification of Pipeline Circuits, Matt Kaufmann and David M. Russinoff, 2000, November. [Technical Report]
A Framework for VHDL Combining Theorem Proving and Symbolic Simulation, Philippe Georgelin and Dominique Borrione and Pierre Ostier, in Proceedings of the Third International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '02), 2002, April. [Conference Paper]
Representing Nuprl Proof Objects in ACL2 : toward a proof checker for Nuprl , James L. Caldwell and John Cowles, in Proceedings of the Third International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '02), 2002, April. [Conference Paper]
Formal Verification of Divide and Square Root Algorithms Using Series Calculation, Jun Sawada, in Proceedings of the Third International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '02), 2002, April. [Conference Paper]
Taylor's Formula with Remainder, Ruben A. Gamboa and Brittany Middleton, in Proceedings of the Third International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '02), 2002, April. [Conference Paper]
Implementation in ACL2 of Well-Founded Polynomial Orderings, I. Medina-Bulo and F. Palomo-Lozano and J. A. Alonso-Jim\'enez, in Proceedings of the Third International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '02), 2002, April. [Conference Paper]
A Theory About First-Order Terms in ACL2 , J. L. Ruiz-Reina and J. A. Alonso and M. J. Hidalgo and F. J. Mart\'in-Mateos, in Proceedings of the Third International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '02), 2002, April. [Conference Paper]
Progress Report: Term Dags Using Stobjs, J. L. Ruiz-Reina and J. A. Alonso and M. J. Hidalgo and F. J. Mart\'in-Mateos, in Proceedings of the Third International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '02), 2002, April. [Conference Paper]
Adding a Total Order to ACL2 , Panagiotis Manolios and Matt Kaufmann, in Proceedings of the Third International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '02), 2002, April. [Conference Paper]
Checking ACL2 Theorems via SAT Checking, Rob Sumners, in Proceedings of the Third International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '02), 2002, April. [Conference Paper]
Efficient Rewriting of Operations on Finite Structures in ACL2 , Matt Kaufmann and Rob Sumners, in Proceedings of the Third International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '02), 2002, April. [Conference Paper]
Consistently Adding Primitive Recursive Definitions in ACL2 , John Cowles, in Proceedings of the Third International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '02), 2002, April. [Conference Paper]
Flat Domains and Recursive Equations in ACL2 , John Cowles, in Proceedings of the Third International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '02), 2002, April. [Conference Paper]
Molecular Computation Models in ACL2 : a Simulation of Lipton's Experiment Solving SAT , F. J. Mart\'in-Mateos and J. A. Alonso and M. J. P\'erez-Jim\'enez and F. Sancho-Caparrini, in Proceedings of the Third International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '02), 2002, April. [Conference Paper]
A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory., F. J. Mart\' i n-Mateos and J. A. Alonso and M. J. Hidalgo and J. L. Ruiz-Reina, in Proceedings of the Third International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '02), 2002, April. [Conference Paper]
Verification of an In-place Quicksort in ACL2 , Sandip Ray and Rob Sumners, in Proceedings of the Third International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '02), 2002, April. [Conference Paper]
A Tool for Simplifying Files of ACL2 Definitions, Matt Kaufmann, in Proceedings of the Fourth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '03), 2003, July. [Conference Paper]
Matricies in ACL2 , Joe Hendrix, in Proceedings of the Fourth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '03), 2003, July. [Conference Paper]
Ordinal Arithmetic in ACL2 , Panagiotis Manolios and Daron Vroon, in Proceedings of the Fourth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '03), 2003, July. [Conference Paper]
Proof of Dickson's Lemma Using the ACL2 Theorem Prover via an Explicit Ordinal Mapping, Matyas Sustik, in Proceedings of the Fourth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '03), 2003, July. [Conference Paper]
Using ACL2 Arrays to Formalize Matrix Algebra, Ruben Gamboa and John Cowles and Jeff Van Baalen, in Proceedings of the Fourth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '03), 2003, July. [Conference Paper]
On the Verification of Synthesized Kalman Filters, Ruben Gamboa and John Cowles and Jeff Van Baalen, in Proceedings of the Fourth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '03), 2003, July. [Conference Paper]
Encapsulation for Practical Simplification Procedures, Olga Shumsky Matlin and William McCune, in Proceedings of the Fourth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '03), 2003, July. [Conference Paper]
Fair Environment Assumptions in ACL2 , Rob Sumners, in Proceedings of the Fourth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '03), 2003, July. [Conference Paper]
SHA Formalization, Diana Toma and Dominique Borrione, in Proceedings of the Fourth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '03), 2003, July. [Conference Paper]
A Separation Kernel Formal Security Policy, David Greve and Matthew Wilding and W. Mark Vanfleet, in Proceedings of the Fourth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '03), 2003, July. [Conference Paper]
Memory Taggings and Dynamic Data Structures, J Strother Moore, in Proceedings of the Fourth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '03), 2003, July. [Conference Paper]
Inductive Assertions and Operational Semantics, J Strother Moore, in Proceedings of the Fourth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '03), 2003, July. [Conference Paper]
Typed ACL2 Records, David Greve and Matthew Wilding, in Proceedings of the Fourth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '03), 2003, July. [Conference Paper]
Using MBE to Speed a Verified Graph Pathfinder, David Greve and Matthew Wilding, in Proceedings of the Fourth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '03), 2003, July. [Conference Paper]
A Solution to the Rockwell Challenge, Hanbing Liu, in Proceedings of the Fourth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '03), 2003, July. [Conference Paper]
Using ACL2 to Verify Security Properties of Specification-based Intrusion Detection Systems, Tao Song and Jim Alves-Foss and Calvin Ko and Cui Zhang and Karl Levitt, in Proceedings of the Fourth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '03), 2003, July. [Conference Paper]
Combining ACL2 and Mathematica for the Symbolic Simulation of Digital Systems, Ghiath Al Sammane and Dominique Borrione and Pierre Ostier and Julien Schmaltz and Diana Toma, in Proceedings of the Fourth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '03), 2003, July. [Conference Paper]
Validation of a Parameterized Bus Architecture Model, Julien Schmaltz and Dominique Borrione, in Proceedings of the Fourth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '03), 2003, July. [Conference Paper]
Polymorphism in ACL2 , Ruben Gamboa and Mark Patterson, in Proceedings of the Fourth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '03), 2003, July. [Conference Paper]
Writing Literate Proofs with XML Tools, Ruben Gamboa, in Proceedings of the Fourth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '03), 2003, July. [Conference Paper]
Certifying Compositional Model Checking Algorithms in ACL2 , Sandip Ray and John Matthews and Mark Tuttle, in Proceedings of the Fourth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '03), 2003, July. [Conference Paper]
Implementing Abstract Types in ACL2 , Vernon Austel, in Proceedings of the Fourth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '03), 2003, July. [Conference Paper]
Reducing Invariant Proofs to Finite Search via Rewriting, Rob Sumners and Sandip Ray, in Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '04), 2004, November. [Conference Paper]
Attaching Efficient Executability to Partial Functions in ACL2 , Sandip Ray, in Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '04), 2004, November. [Conference Paper]
Partial Clock Functions in ACL2 , John Matthews and Daron Vroon, in Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '04), 2004, November. [Conference Paper]
Formally Verifying an Algorithm Based on Interval Arithmetic for Checking Transversality, Marcio Gameiro and Panagiotis Manolios, in Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '04), 2004, November. [Conference Paper]
A Suite of Hard ACL2 Theorems Arising in Refinement-Based Processor Verification, Panagiotis Manolios and Sudarshan K. Srinivasan, in Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '04), 2004, November. [Conference Paper]
Finite Set Theory based on Fully Ordered Lists, Jared Davis, in Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '04), 2004, November. [Conference Paper]
Verifying Transformation Rules of the HATS High-Assurance Transformation System: An Approach, Steve Roach and Fares Fraij, in Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '04), 2004, November. [Conference Paper]
A Case Study in using ACL2 for Feature-Oriented Verification, Kathi Fisler and Brian Roberts, in Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '04), 2004, November. [Conference Paper]
ACL2VHDL Translator: A Simple Approach to Fill the Semantic Gap, Jun Sawada, in Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '04), 2004, November. [Conference Paper]
Adding a typing mechanism to ACL2 , Vernon Austel, in Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and Its Applications ( ACL2 '04), 2004, November. [Conference Paper]
A Formally Verified Quadratic Unification Algorithm, J. L. Ruiz Reina and J. A. Alonso and M. J. Hidalgo and F. J. Mart\'in-Mateos, in Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '04), 2004, November. [Conference Paper]
Generic Theories as Proof Strategies: A Case Study for Weakest Precondition Style Proofs, Wilfred Legato, in Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '04), 2004, November. [Conference Paper]
Integrating Nonlinear Arithmetic into ACL2 , Warren A. Hunt, Jr. and Robert Bellarmine Krug and J Moore, in Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '04), 2004, November. [Conference Paper]
A Summary of Intrinsic Partitioning Verification, David Greve and Raymond Richards and Matthew Wilding, in Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '04), 2004, November. [Conference Paper]
Address Enumeration and Reasoning Over Linear Address Spaces, David Greve, in Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '04), 2004, November. [Conference Paper]
An ACL2 Library for Bags (Multisets), Eric Smith and Serita Nelesen and David Greve and Matthew Wilding and Raymond Richards, in Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '04), 2004, November. [Conference Paper]
The Common Criteria , Formal Methods and ACL2 , Raymond Richards and David Greve and Matthew Wilding, in Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '04), 2004, November. [Conference Paper]
Reverse Abstraction in ACL2 , Bill Young, in Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '04), 2004, November. [Conference Paper]
An Analysis of the GWV Security Policy, Jim Alves-Foss and Carol Taylor, in Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '04), 2004, November. [Conference Paper]
A Functional Specification and Validation Model for Networks on Chip in the ACL2 Logic, Julien Schmaltz and Dominique Borrione, in Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '04), 2004, November. [Conference Paper]
Verification of a Cryptographic Circuit: SHA-1 using ACL2 , Diana Toma and Dominique Borrione, in Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '04), 2004, November. [Conference Paper]
Axiomatic Events in ACL2(r) : A Story of defun, defun-std, and encapsulate, Ruben Gamboa and John Cowles and Nadya Kuzmina, in Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '04), 2004, November. [Conference Paper]
Contributions to the Theory of Tail Recursive Functions, John Cowles and Ruben Gamboa, in Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '04), 2004, November. [Conference Paper]
A Verifying Core for a Cryptographic Language Compiler, Lee Pike and Mark Shields and John Matthews, in Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '06), 2006, August. [Conference Paper]
A Robust Machine Code Proof Framework for Highly Secure Applications, David S. Hardin and Eric W. Smith and William D. Young, in Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '06), 2006, August. [Conference Paper]
Unique Factorization in ACL2 : Euclidean Domains, John Cowles and Ruben Gamboa, in Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '06), 2006, August. [Conference Paper]
Parameterized Congruences in ACL2 , David Greve, in Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '06), 2006, August. [Conference Paper]
Soundness of the Simply Typed Lambda Calculus in ACL2 , Sol Swords and William R. Cook, in Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '06), 2006, August. [Conference Paper]
An Embedding of the ACL2 Logic in HOL , Mike Gordon and Warren A. Hunt, Jr. and Matt Kaufmann and James Reynolds, in Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '06), 2006, August. [Conference Paper]
Towards a Formal Theory of On Chip Communications in the ACL2 Logic, Julien Schmaltz and Dominique Borrione, in Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '06), 2006, August. [Conference Paper]
Memories: Array-like Records for ACL2 , Jared Davis, in Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '06), 2006, August. [Conference Paper]
The Ideal of Verified Software, Tony Hoare, in Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '06), 2006, August. [Conference Paper]
Combining ACL2 and an Automated Verification Tool to Verify a Multiplier, Erik Reeber and Jun Sawada, in Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '06), 2006, August. [Conference Paper]
Implementing a Cost-Aware Evaluator for ACL2 Expressions, Ruben Gamboa and John Cowles, in Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '06), 2006, August. [Conference Paper]
Function Memoization and Unique Object Representation for ACL2 Functions, Robert S. Boyer and Warren A. Hunt, Jr. , in Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '06), 2006, August. [Conference Paper]
Adding Parallelism Capabilities to ACL2 , David L. Rager, in Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '06), 2006, August. [Conference Paper]
Quantification in Tail-recursive Function Definitions, Sandip Ray, in Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '06), 2006, August. [Conference Paper]
Phylogenetic Trees in ACL2 , Warren A. Hunt, Jr. and Serita M. Nelesen, in Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '06), 2006, August. [Conference Paper]
Double Rewriting for Equivalential Reasoning in ACL2 , Matt Kaufmann and J Strother Moore, in Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '06), 2006, August. [Conference Paper]
ACL2 in DrScheme , Dale Vaillancourt and Rex Page and Matthias Felleisen, in Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '06), 2006, August. [Conference Paper]
Reasoning about ACL2 File Input, Jared Davis, in Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '06), 2006, August. [Conference Paper]
A SAT -Based Procedure for Verifying Finite State Machines in ACL2 , Erik Reeber and Warren A. Hunt, Jr. , in Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '06), 2006, August. [Conference Paper]
Hacking and Extending ACL2 , Peter Dillinger and Matt Kaufmann and Pete Manolios, in Proceedings of the Seventh International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '07), 2007, November. [Conference Paper]
Pythia: Automatic Generation of Counterexamples for ACL2 using Alloy , Alexander Spiridonov and Sarfraz Khurshid, in Proceedings of the Seventh International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '07), 2007, November. [Conference Paper]
Backtracking and Induction in ACL2 , John Erickson, in Proceedings of the Seventh International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '07), 2007, November. [Conference Paper]
The While-language Challenge: First Progress, John Cowles and David Greve and William Young, in Proceedings of the Seventh International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '07), 2007, November. [Conference Paper]
Building Lemmas Using Examples, Gabriel Infante - Lopez, in Proceedings of the Seventh International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '07), 2007, November. [Conference Paper]
Formalizing Simplicial Topology in ACL2 , Mirian Andres and Laureano Lamban and Julio Rubio and Jose Luis Ruiz-Reina, in Proceedings of the Seventh International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '07), 2007, November. [Conference Paper]
Formal Specification and Validation of Minimal Routing Algorithms for the 2D Mesh, Julien Schmaltz, in Proceedings of the Seventh International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '07), 2007, November. [Conference Paper]
A Study of Some Flawed Adders, Warren A. Hunt, Jr. and Robert S. Boyer, in Proceedings of the Seventh International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '07), 2007, November. [Conference Paper]
Defining a LISP Interpreter in a Logic of Total Functions, Mike Gordon, in Proceedings of the Seventh International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '07), 2007, November. [Conference Paper]
ACL2 for Freshmen: First Experiences, Carl Eastlund and Dale Vaillancourt and Matthias Felleisen, in Proceedings of the Seventh International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '07), 2007, November. [Conference Paper]
Evolution from Debugging to Verification, Frank Rimlinger, in Proceedings of the Seventh International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '07), 2007, November. [Conference Paper]
Scalable Normalization for Heap Manipulating Functions, David Greve, in Proceedings of the Seventh International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '07), 2007, November. [Conference Paper]
A Generalized Solution for the While Challenge, Sandip Ray, in Proceedings of the Seventh International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '07), 2007, November. [Conference Paper]
Proof Reusing: The Case of the Hindley Algorithm, Diego Sotes and Laureano Lamban and Julio Rubio, in Proceedings of the Seventh International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '07), 2007, November. [Conference Paper]
User Control and Direction of a More Efficient Simplifier in ACL2 , Rob Sumners, in Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '09), 2009, May. [Conference Paper]
Automatically Computing Functional Instantiations, J Moore, in Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '09), 2009, May. [Conference Paper]
Symbolic Simulation in ACL2 , Robert S. Boyer and Warren A. Hunt, Jr. , in Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '09), 2009, May. [Conference Paper]
Proving A Specific Type Of Inequality Theorems in ACL2 : a bind-free experience report, Hanbing Liu, in Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '09), 2009, May. [Conference Paper]
Computational Logic in the Undergraduate Curriculum, Rex Page, in Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '09), 2009, May. [Conference Paper]
Automatic Verification for Interactive Graphical Programs, Carl Eastlund and Matthias Felleisen, in Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '09), 2009, May. [Conference Paper]
DoubleCheck Your Theorems, Carl Eastlund, in Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '09), 2009, May. [Conference Paper]
Hypertext Navigation of ACL2 Proofs with XMLEye , Antonio Garcia - Dominguez and Francisco Palomo - Lozaon and Inmaculada Medina - Bulo, in Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '09), 2009, May. [Conference Paper]
Inverse Functions in ACL2(r) , Ruben Gamboa and John Cowles, in Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '09), 2009, May. [Conference Paper]
Abbreviated Output for Input in ACL2 : An Implementation Case Study, Matt Kaufmann, in Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '09), 2009, May. [Conference Paper]
ACL2 -Certified AVL Trees, Ryan Ralston, in Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '09), 2009, May. [Conference Paper]
Proof of Transitive Closure Property of Directed Acyclic Graphs, Fares Fraij and Steve Roach, in Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '09), 2009, May. [Conference Paper]
Solving $\triangle = \square$, John Cowles and Ruben Gamboa, in Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '09), 2009, May. [Conference Paper]
Formal Verification of LabVIEW Programs Using the ACL2 Theorem Prover, Matt Kaufmann and Jacob Kornerup and Mark Reitblatt, in Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '09), 2009, May. [Conference Paper]
ACL2 for the Verification of Fault-Tolerance Properties: First Results, Laurence Pierre and Renauld Clavel and Regis Leveugle, in Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '09), 2009, May. [Conference Paper]
Efficient, Formally Verifiable Data Structures using ACL2 Single-Threaded Objects for High-Assurance Systems, David Hardin and Samuel Hardin, in Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '09), 2009, May. [Conference Paper]
An Executable Model for Security Protocol JFKr , David Rager, in Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '09), 2009, May. [Conference Paper]
Automated Reasoning With Quantified Formulae, Dave Greve, in Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '09), 2009, May. [Conference Paper]
Assuming Termination, Dave Greve, in Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '09), 2009, May. [Conference Paper]
A Generic Implementation Model for the Formal Verification of Networks-on-Chips, Tom van der Broek and Julien Schmaltz, in Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '09), 2009, May. [Conference Paper]
Formal Validation of Deadlock Prevention in Networks-on-Chips, Freek Verbeek and Julien Schmaltz, in Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '09), 2009, May. [Conference Paper]
A Formally Verified OS Kernel. Now What?, Gerwin Klein, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
Proof Assistants as Teaching Assistants: A View from the Trenches, Benjamin C. Pierce, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
A Certified Denotational Abstract Interpreter, David Cachera and David Pichardie, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
Using a First Order Logic to Verify That Some Set of Reals Has No Lebesgue Measure, John Cowles and Ruben Gamboa, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
A New Foundation for Nominal Isabelle , Brian Huffman and Christian Urban, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
(Nominal) Unification by Recursive Descent with Triangular Substitution, Ramana Kumar and Michael Norrish, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks, Freek Verbeek and Julien Schmaltz, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
Untitled, Micha\, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
A Tactic Language for Declarative Proofs, Serge Autexier and Dominik Dietrich, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
Programming Language Techniques for Cryptographic Proofs, Gilles Barthe and Benjamin Gr\'egoire and Santiago Zanella B\'eguelin, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder, Jasmin Christian Blanchette and Tobias Nipkow, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
Formal Proof of a Wave Equation Resolution Scheme: The Method Error, Sylvie Boldo and Fran\c c ois Cl\'ement and Jean-Christophe Filli\^atre and Micaela Mayero and Guillaume Melquiond and Pierre Weis, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
An Efficient Coq Tactic for Deciding Kleene Algebras, Thomas Braibant and Damien Pous, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
Untitled, Sascha B\, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
The Optimal Fixed Point Combinator, Arthur Chargu\'eraud, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
Formal Study of Plane Delaunay Triangulation, Jean-Fran\c c ois Dufourd and Yves Bertot, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison, Amy Felty and Brigitte Pientka, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture, Anthony Fox and Magnus O. Myreen, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
Automated Machine-Checked Hybrid System Safety Proofs, Herman Geuvers and Adam Koprowski and Dan Synek and Eelis van der Weegen, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
Coverset Induction with Partiality and Subsorts: A Powerlist Case Study, Joe Hendrix and Deepak Kapur and Jos\'e Meseguer, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
Case-Analysis for Rippling and Inductive Proof, Moa Johansson and Lucas Dixon and Alan Bundy, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
Importing HOL Light into Coq , Chantal Keller and Benjamin Werner, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
A Mechanized Translation from Higher-Order Logic to Set Theory, Alexander Krauss and Andreas Schropp, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
The Isabelle Collections Framework, Peter Lammich and Andreas Lochbihler, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
Interactive Termination Proofs Using Termination Cores, Panagiotis Manolios and Daron Vroon, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
A Framework for Formal Verification of Compiler Optimizations, William Mansky and Elsa Gunter, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
On the Formalization of the Lebesgue Integration Theory in HOL , Tarek Mhamdi and Osman Hasan and Sofi\`ene Tahar, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
From Total Store Order to Sequential Consistency: A Practical Reduction Theorem, Ernie Cohen and Bert Schirmer, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
Equations: A Dependent Pattern-Matching Compiler, Matthieu Sozeau, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
A Mechanically Verified AIG -to- BDD Conversion Algorithm, Sol Swords and Warren A. Hunt, Jr. , in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
Inductive Consequences in the Calculus of Constructions , Daria Walukiewicz-Chrz\k a szcz and Jacek Chrz\k a szcz, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
Validating QBF Invalidity in HOL4 , Tjark Weber, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
Higher-Order Abstract Syntax in Isabelle/HOL , Douglas J. Howe, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
Separation Logic Adapted for Proofs by Rewriting, Magnus O. Myreen, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
Developing the Algebraic Hierarchy with Type Classes in Coq , Bas Spitters and Eelis van der Weegen, in Proceedings of the First International Conference on Interactive Theorem Proving ( ITP '10), 2010, July. [Conference Paper]
Integrating Testing and Interactive Theorem Proving, Harsh Raju Chamarthi and Peter C. Dillinger and Matt Kaufmann and Panagiotis Manolios, in Proceedings of the Tenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '11), 2011, November. [Conference Paper]
Verifying Sierpi\'nski and Riesel Numbers in ACL2 , John R. Cowles and Ruben Gamboa, in Proceedings of the Tenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '11), 2011, November. [Conference Paper]
Toward the Verification of a Simple Hypervisor, Mike Dahlin and Ryan Johnson and Robert Bellarmine Krug and Michael McCoyd and William Young, in Proceedings of the Tenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '11), 2011, November. [Conference Paper]
How Can I Do That with ACL2 ? Recent Enhancements to ACL2 , Matt Kaufmann and J Strother Moore, in Proceedings of the Tenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '11), 2011, November. [Conference Paper]
Implementing an Automatic Differentiator in ACL2 , Peter Reid and Ruben Gamboa, in Proceedings of the Tenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '11), 2011, November. [Conference Paper]
Formal Verification of an Iterative Low-Power x86 Floating-Point Multiplier with Redundant Feedback, Peter - Michael Seidel, in Proceedings of the Tenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '11), 2011, November. [Conference Paper]
Bit-Blasting ACL2 Theorems, Sol Swords and Jared Davis, in Proceedings of the Tenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '11), 2011, November. [Conference Paper]
Formal verification of a deadlock detection algorithm, Freek Verbeek and Julien Schmaltz, in Proceedings of the Tenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '11), 2011, November. [Conference Paper]
Embedding ACL2 Models in End-User Applications, Jared Davis, in Proceedings of the Eleventh International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '13), 2013, May. [Conference Paper]
Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1, Matt Kaufmann and J Strother Moore, in Proceedings of the Eleventh International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '13), 2013, May. [Conference Paper]
Proof Pad : A New Development Environment for ACL2 , Caleb Eggensperger, in Proceedings of the Eleventh International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '13), 2013, May. [Conference Paper]
A Macro for Reusing Abstract Functions and Theorems, Sebastiaan J. C. Joosten and Bernard van Gastel and Julien Schmaltz, in Proceedings of the Eleventh International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '13), 2013, May. [Conference Paper]
A Step-Indexing Approach to Partial Functions, David Greve and Konrad Slind, in Proceedings of the Eleventh International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '13), 2013, May. [Conference Paper]
Abstract Stobjs and Their Application to ISA Modeling, Shilpi Goel and Warren A. Hunt, Jr. and Matt Kaufmann, in Proceedings of the Eleventh International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '13), 2013, May. [Conference Paper]
Verification of Building Blocks for Asynchronous Circuits, Freek Verbeek and Julien Schmaltz, in Proceedings of the Eleventh International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '13), 2013, May. [Conference Paper]
An Interpreter for Quantum Circuits, Lucas Helms and Ruben Gamboa, in Proceedings of the Eleventh International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '13), 2013, May. [Conference Paper]
Verified AIG Algorithms in ACL2 , Jared Davis and Sol Swords, in Proceedings of the Eleventh International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '13), 2013, May. [Conference Paper]
A formalisation of XMAS , Bernard van Gastel and Julien Schmaltz, in Proceedings of the Eleventh International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '13), 2013, May. [Conference Paper]
ACL2 Meets the GPU : Formalizing a CUDA -based Parallelizable All-Pairs Shortest Path Algorithm in ACL2 , David S. Hardin and Samuel S. Hardin, in Proceedings of the Eleventh International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '13), 2013, May. [Conference Paper]
Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4, Matt Kaufmann and J Strother Moore, in Proceedings of the Twelfth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '14), 2014, July. [Conference Paper]
Industrial-Strength Documentation for ACL2 , Jared Davis and Matt Kaufmann, in Proceedings of the Twelfth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '14), 2014, July. [Conference Paper]
Data Definitions in the ACL2 Sedan , Harsh Raju Chamarthi and Peter C. Dillinger and Panagiotis Manolios, in Proceedings of the Twelfth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '14), 2014, July. [Conference Paper]
Polymorphic Types in ACL2 , Benjamin Selfridge and Eric Smith, in Proceedings of the Twelfth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '14), 2014, July. [Conference Paper]
ACL2(ml) : Machine-Learning for ACL2 , J\'onathan Heras and Ekaterina Komendantskaya, in Proceedings of the Twelfth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '14), 2014, July. [Conference Paper]
Initial Experiments with TPTP -style Automated Theorem Provers on ACL2 Problems, Sebastiaan Joosten and Cezary Kaliszyk and Josef Urban, in Proceedings of the Twelfth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '14), 2014, July. [Conference Paper]
On Vickrey 's Theorem and the Use of ACL2 for Formal Reasoning in Economics, Ruben Gamboa and John Cowles, in Proceedings of the Twelfth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '14), 2014, July. [Conference Paper]
Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis, John Cowles and Ruben Gamboa, in Proceedings of the Twelfth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '14), 2014, July. [Conference Paper]
Formal Verification of Medina 's Sequence of Polynomials for Approximating Arctangent, Ruben Gamboa and John Cowles, in Proceedings of the Twelfth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '14), 2014, July. [Conference Paper]
Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis, Disha Puri and Sandip Ray and Kecheng Hao and Fei Xie, in Proceedings of the Twelfth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '14), 2014, July. [Conference Paper]
An ACL2 Mechanization of an Axiomatic Framework for Weak Memory, Benjamin Selfridge, in Proceedings of the Twelfth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '14), 2014, July. [Conference Paper]
Modeling Algorithms in SystemC and ACL2 , John W. O'Leary and David M. Russinoff, in Proceedings of the Twelfth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '14), 2014, July. [Conference Paper]
Development of a Translator from LLVM to ACL2 , David S. Hardin and Jennifer A. Davis and David A. Greve and Jedidiah R. McClurg, in Proceedings of the Twelfth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '14), 2014, July. [Conference Paper]
A Brief Introduction to Oracle 's Use of ACL2 in Verifying Floating-point and Integer Arithmetic, David L. Rager and Jo Ebergen and Austin Lee and Dmitry Nadezhin and Ben Selfridge and Cuong K. Chau, in Proceedings of the Thirteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '15), 2015, October. [Conference Paper]
Fix Your Types, Sol Swords and Jared Davis, in Proceedings of the Thirteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '15), 2015, October. [Conference Paper]
Second-Order Functions and Theorems in ACL2 , Alessandro Coglio, in Proceedings of the Thirteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '15), 2015, October. [Conference Paper]
Fourier Series Formalization in ACL2(r) , Cuong K. Chau and Matt Kaufmann and Warren A. Hunt, Jr. , in Proceedings of the Thirteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '15), 2015, October. [Conference Paper]
Perfect Numbers in ACL2 , John Cowles and Ruben Gamboa, in Proceedings of the Thirteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '15), 2015, October. [Conference Paper]
Extending ACL2 with SMT Solvers, Yan Peng and Mark Greenstreet, in Proceedings of the Thirteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '15), 2015, October. [Conference Paper]
Reasoning about LLVM Code Using Codewalker , David S. Hardin, in Proceedings of the Thirteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '15), 2015, October. [Conference Paper]
Stateman : Using Metafunctions to Manage Large Terms Representing Machine States, J Strother Moore, in Proceedings of the Thirteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '15), 2015, October. [Conference Paper]
Proving Skipping Refinement with ACL2s , Mitesh Jain and Panagiotis Manolios, in Proceedings of the Thirteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '15), 2015, October. [Conference Paper]
The x86isa Books: Features, Usage, and Future Plans, Shilpi Goel, in Proceedings of the Fourteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '17), 2017, May. [Conference Paper]
The Cayley-Dickson Construction in ACL2 , John Cowles and Ruben Gamboa, in Proceedings of the Fourteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '17), 2017, May. [Conference Paper]
A Computationally Surveyable Proof of the Group Properties of an Elliptic Curve, David M. Russinoff, in Proceedings of the Fourteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '17), 2017, May. [Conference Paper]
Meta-extract: Using Existing Facts in Meta-reasoning, Matt Kaufmann and Sol Swords, in Proceedings of the Fourteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '17), 2017, May. [Conference Paper]
A Versatile, Sound Tool for Simplifying Definitions, Alessandro Coglio and Matt Kaufmann and Eric W. Smith, in Proceedings of the Fourteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '17), 2017, May. [Conference Paper]
Proof Reduction of Fair Stuttering Refinement of Asynchronous Systems and Applications, Rob Sumners, in Proceedings of the Fourteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '17), 2017, May. [Conference Paper]
Term-Level Reasoning in Support of Bit-blasting, Sol Swords, in Proceedings of the Fourteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '17), 2017, May. [Conference Paper]
Formal Specification and Verification of the FM9001 Microprocessor Using the DE System, Cuong Chau, in Proceedings of the Fourteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '17), 2017, May. [Conference Paper]
A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java, Alessandro Coglio, in Proceedings of the Fifteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '18), 2018, November, DOI: 10.4204/EPTCS.280.1. [Conference Paper]
Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32 , Mihir Parang Mehta, in Proceedings of the Fifteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '18), 2018, November, DOI: 10.4204/EPTCS.280.2. [Conference Paper]
Trapezoidal Generalization over Linear Constraints, David A. Greve and Andrew Gacek, in Proceedings of the Fifteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '18), 2018, November, DOI: 10.4204/EPTCS.280.3. [Conference Paper]
Incremental SAT Library Integration Using Abstract Stobjs, Sol Swords, in Proceedings of the Fifteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '18), 2018, November, DOI: 10.4204/EPTCS.280.4. [Conference Paper]
Using ACL2 in the Design of Efficient, Verifiable Data Structures for High-Assurance Systems, David S. Hardin and Konrad Slind, in Proceedings of the Fifteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '18), 2018, November, DOI: 10.4204/EPTCS.280.5. [Conference Paper]
Adding 32-bit Mode to the ACL2 Model of the x86 ISA , Alessandro Coglio and Shilpi Goel, in Proceedings of the Fifteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '18), 2018, November, DOI: 10.4204/EPTCS.280.6. [Conference Paper]
A Toolbox For Property Checking From Simulation Using Incremental SAT (Extended Abstract), Rob Sumners, in Proceedings of the Fifteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '18), 2018, November, DOI: 10.4204/EPTCS.280.7. [Conference Paper]
The Fundamental Theorem of Algebra in ACL2 , Ruben Gamboa and John R. Cowles, in Proceedings of the Fifteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '18), 2018, November, DOI: 10.4204/EPTCS.280.8. [Conference Paper]
Real Vector Spaces and the Cauchy-Schwarz Inequality in ACL2 (r), Carl Kwan and Mark R. Greenstreet, in Proceedings of the Fifteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '18), 2018, November, DOI: 10.4204/EPTCS.280.9. [Conference Paper]
Convex Functions in ACL2 (r), Carl Kwan and Mark R. Greenstreet, in Proceedings of the Fifteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '18), 2018, November, DOI: 10.4204/EPTCS.280.10. [Conference Paper]
Smtlink 2.0, Yan Peng and Mark R. Greenstreet, in Proceedings of the Fifteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '18), 2018, November, DOI: 10.4204/EPTCS.280.11. [Conference Paper]
DefunT : A Tool for Automating Termination Proofs by Using the Community Books (Extended Abstract), Matt Kaufmann, in Proceedings of the Fifteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '18), 2018, November, DOI: 10.4204/EPTCS.280.12. [Conference Paper]
Hint Orchestration Using ACL2 's Simplifier, Sol Swords, in Proceedings of the Fifteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '18), 2018, November, DOI: 10.4204/EPTCS.280.13. [Conference Paper]
Formal Verification of Arithmetic RTL: Translating Verilog to C++ to ACL2 , David M. Russinoff, in Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '20), 2020, May, DOI: 10.4204/EPTCS.327.1. [Conference Paper]
Iteration in ACL2 , Matt Kaufmann and J Strother Moore, in Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '20), 2020, May, DOI: 10.4204/EPTCS.327.2. [Conference Paper]
New Rewriter Features in FGL , Sol Swords, in Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '20), 2020, May, DOI: 10.4204/EPTCS.327.3. [Conference Paper]
Computing and Proving Well-founded Orderings through Finite Abstractions, Rob Sumners, in Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '20), 2020, May, DOI: 10.4204/EPTCS.327.4. [Conference Paper]
RP-Rewriter: An Optimized Rewriter for Large Terms in ACL2 , Mertcan Temel, in Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '20), 2020, May, DOI: 10.4204/EPTCS.327.5. [Conference Paper]
Quadratic Extensions in ACL2 , Ruben Gamboa and John R. Cowles and Woodrow Gamboa, in Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '20), 2020, May, DOI: 10.4204/EPTCS.327.6. [Conference Paper]
Type Inference Using Meta-extract for Smtlink and Beyond, Yan Peng and Mark R. Greenstreet, in Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '20), 2020, May, DOI: 10.4204/EPTCS.327.7. [Conference Paper]
Cauchy-Schwarz in ACL2 (r) Abstract Vector Spaces, Carl Kwan and Yan Peng and Mark R. Greenstreet, in Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '20), 2020, May, DOI: 10.4204/EPTCS.327.8. [Conference Paper]
Minimal Fractional Representations of Integers mod M, David Greve, in Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '20), 2020, May, DOI: 10.4204/EPTCS.327.9. [Conference Paper]
Generating Mutually Inductive Theorems from Concise Descriptions, Sol Swords, in Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '20), 2020, May, DOI: 10.4204/EPTCS.327.10. [Conference Paper]
Ethereum's Recursive Length Prefix in ACL2 , Alessandro Coglio, in Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '20), 2020, May, DOI: 10.4204/EPTCS.327.11. [Conference Paper]
Isomorphic Data Type Transformations, Alessandro Coglio and Stephen J. Westfold, in Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '20), 2020, May, DOI: 10.4204/EPTCS.327.12. [Conference Paper]
Put Me on the RAC , David Hardin, in Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '20), 2020, May, DOI: 10.4204/EPTCS.327.13. [Conference Paper]
Extended Abstract: Stobj-tables, Matt Kaufmann and Rob Sumners and Sol Swords, in Proceedings of the Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '22), 2022, May, DOI: 10.4204/EPTCS.359.1. [Conference Paper]
Extended Abstract: Iteration in ACL2 , WITH .. DO , Matt Kaufmann and J Strother Moore, in Proceedings of the Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '22), 2022, May, DOI: 10.4204/EPTCS.359.2. [Conference Paper]
All Prime Numbers Have Primitive Roots, Ruben Gamboa and Woodrow Gamboa, in Proceedings of the Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '22), 2022, May, DOI: 10.4204/EPTCS.359.3. [Conference Paper]
Using ACL2 To Teach Students About Software Testing, Ruben Gamboa and Alicia Thoney, in Proceedings of the Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '22), 2022, May, DOI: 10.4204/EPTCS.359.4. [Conference Paper]
A Mechanized Proof of Bounded Convergence Time for the Distributed Perimeter Surveillance System (DPSS) Algorithm A , David A. Greve and Jennifer A. Davis and Laura R. Humphrey, in Proceedings of the Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '22), 2022, May, DOI: 10.4204/EPTCS.359.5. [Conference Paper]
Properties of the Hebrew Calendar, David M. Russinoff, in Proceedings of the Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '22), 2022, May, DOI: 10.4204/EPTCS.359.6. [Conference Paper]
VWSIM: A Circuit Simulator, Warren A. Hunt Jr. and Vivek Ramanathan and J Strother Moore, in Proceedings of the Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '22), 2022, May, DOI: 10.4204/EPTCS.359.7. [Conference Paper]
A Free Group of Rotations of Rank 2, Jagadish Bapanapally and Ruben Gamboa, in Proceedings of the Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '22), 2022, May, DOI: 10.4204/EPTCS.359.8. [Conference Paper]
Modeling Asymptotic Complexity Using ACL2 , William D. Young, in Proceedings of the Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '22), 2022, May, DOI: 10.4204/EPTCS.359.9. [Conference Paper]
A Formalization of Finite Group Theory, David M. Russinoff, in Proceedings of the Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '22), 2022, May, DOI: 10.4204/EPTCS.359.10. [Conference Paper]
Verified Implementation of an Efficient Term-Rewriting Algorithm for Multiplier Verification on ACL2 , Mertcan Temel, in Proceedings of the Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '22), 2022, May, DOI: 10.4204/EPTCS.359.11. [Conference Paper]
ACL2s Systems Programming, Andrew T. Walter and Panagiotis Manolios, in Proceedings of the Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '22), 2022, May, DOI: 10.4204/EPTCS.359.12. [Conference Paper]
Syntheto: A Surface Language for APT and ACL2 , Alessandro Coglio and Eric McCarthy and Stephen J. Westfold and Daniel Balasubramanian and Abhishek Dubey and Gabor Karsai, in Proceedings of the Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '22), 2022, May, DOI: 10.4204/EPTCS.359.13. [Conference Paper]
A Complex Java Code Generator for ACL2 Based on a Shallow Embedding of ACL2 in Java, Alessandro Coglio, in Proceedings of the Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '22), 2022, May, DOI: 10.4204/EPTCS.359.14. [Conference Paper]
A Proof-Generating C Code Generator for ACL2 Based on a Shallow Embedding of C in ACL2 , Alessandro Coglio, in Proceedings of the Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '22), 2022, May, DOI: 10.4204/EPTCS.359.15. [Conference Paper]
Hardware/Software Co-Assurance using the Rust Programming Language and ACL2 , David S. Hardin, in Proceedings of the Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '22), 2022, May, DOI: 10.4204/EPTCS.359.16. [Conference Paper]
Extended Abstract: Classical LU Decomposition in ACL2 , Carl Kwan, in Proceedings of the Eighteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '23), 2023, November, DOI: 10.4204/EPTCS.393.1. [Conference Paper]
Extended Abstract: CHERI Concentrate in ACL2 , Carl Kwan and Yutong Xin and William D. Young, in Proceedings of the Eighteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '23), 2023, November, DOI: 10.4204/EPTCS.393.2. [Conference Paper]
Extended Abstract: A Bound-Finding Tool for Arithmetic Terms, Sol Swords, in Proceedings of the Eighteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '23), 2023, November, DOI: 10.4204/EPTCS.393.3. [Conference Paper]
A Formalization of Finite Group Theory: Part II , David M. Russinoff, in Proceedings of the Eighteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '23), 2023, November, DOI: 10.4204/EPTCS.393.4. [Conference Paper]
A Formalization of Finite Group Theory: Part III , David M. Russinoff, in Proceedings of the Eighteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '23), 2023, November, DOI: 10.4204/EPTCS.393.5. [Conference Paper]
A Case Study in Analytic Protocol Analysis in ACL2 , Max von Hippel and Panagiotis Manolios and Kenneth L. McMillan and Cristina Nita - Rotaru and Lenore D. Zuck, in Proceedings of the Eighteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '23), 2023, November, DOI: 10.4204/EPTCS.393.6. [Conference Paper]
Advances in ACL2 Proof Debugging Tools, Matt Kaufmann and J Strother Moore, in Proceedings of the Eighteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '23), 2023, November, DOI: 10.4204/EPTCS.393.7. [Conference Paper]
Using Counterexample Generation and Theory Exploration to Suggest Missing Hypotheses, Ruben Gamboa and Panagiotis Manolios and Eric Whitman Smith and Kyle Thompson, in Proceedings of the Eighteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '23), 2023, November, DOI: 10.4204/EPTCS.393.8. [Conference Paper]
Formal Verification of Zero-Knowledge Circuits, Alessandro Coglio and Eric McCarthy and Eric Whitman Smith, in Proceedings of the Eighteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '23), 2023, November, DOI: 10.4204/EPTCS.393.9. [Conference Paper]
Verification of GossipSub in ACL2s , Ankit Kumar and Max von Hippel and Panagiotis Manolios and Cristina Nita - Rotaru, in Proceedings of the Eighteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '23), 2023, November, DOI: 10.4204/EPTCS.393.10. [Conference Paper]
Proving Calculational Proofs Correct, Andrew T. Walter and Ankit Kumar and Panagiotis Manolios, in Proceedings of the Eighteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '23), 2023, November, DOI: 10.4204/EPTCS.393.11. [Conference Paper]
ACL2 Proofs of Nonlinear Inequalities with Imandra, Grant O. Passmore, in Proceedings of the Eighteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '23), 2023, November, DOI: 10.4204/EPTCS.393.12. [Conference Paper]
Verification of a Rust Implementation of Knuth's Dancing Links using ACL2 , David S. Hardin, in Proceedings of the Eighteenth International Workshop on the ACL2 Theorem Prover and its Applications ( ACL2 '23), 2023, November, DOI: 10.4204/EPTCS.393.13. [Conference Paper]