ACL2

swMATH60WikidataQ4650692 ScholiaQ4650692MaRDI QIDQ12833FDOQ12833

Author name not available (Why is that?)

Described by source

• Towards a mechanically checked theory of computation. The ACL2 project

Cited In (only showing first 100 items - show all)

• The seventeen provers of the world. Foreword by Dana S. Scott..
• Using Open Mathematical Documents to Interface Computer Algebra and Proof Assistant Systems
• Title not available (Why is that?)
• Logic-based program synthesis and transformation. 20th international symposium, LOPSTR 2010, Hagenberg, Austria, July 23--25, 2010. Revised selected papers
• Title not available (Why is that?)
• CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver
• On the desirability of mechanizing calculational proofs
• Automatic Differentiation in ACL2
• Title not available (Why is that?)
• The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4
• Adapting functional programs to higher order logic
• Title not available (Why is that?)
• Formal Methods in Computer-Aided Design
• Specification and verification of concurrent programs through refinements
• A formalization of powerlist algebra in ACL2
• Directly reflective meta-programming
• The proof monad
• Automated Deduction – CADE-19
• Principles of proof scores in CafeOBJ
• Superposition with structural induction
• Computer Aided Verification
• Correct Hardware Design and Verification Methods
• A verified compiler from Isabelle/HOL to CakeML
• Toward automating the discovery of decreasing measures
• A graph library for Isabelle
• Computer theorem proving in mathematics
• System-level non-interference of constant-time cryptography. I: Model
• Systems specification by basic protocols
• Automatic Functional Correctness Proofs for Functional Search Trees
• Verifying distributed systems
• Title not available (Why is that?)
• A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures
• Formal correctness of a quadratic unification algorithm
• Efficient certified RAT verification
• A formalization of the Knuth-Bendix(-Huet) critical pair theorem
• Trace-based verification of imperative programs with I/O
• Inference Rules for Proving the Equivalence of Recursive Procedures
• Computer-Aided Verification for Iterative Matrix Inversion Problems in Systems and Control
• ACL2s: ``the ACL2 sedan
• A complete axiom system for propositional projection temporal logic with cylinder computation model
• Expressing Symmetry Breaking in DRAT Proofs
• System-on-chip methodologies \& design languages. 3rd international conference, FDL 2000, Tübingen, Germany, 2000
• Verifying Refutations with Extended Resolution
• A Sound Semantics for OCaml light
• A Parallelized Theorem Prover for a Logic with Parallel Execution
• Certifying compilers using higher-order theorem provers as certificate checkers
• Reasoning about memory layouts
• Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers
• Theorem Proving in Higher Order Logics
• Formal proofs about rewriting using ACL2
• Formal Methods in Computer-Aided Design
• Formal Methods in Computer-Aided Design
• An ACL2 Tutorial
• Interactive theorem proving. Second international conference, ITP 2011, Berg en Dal, The Netherlands, August 22--25, 2011. Proceedings
• A mechanical analysis of program verification strategies
• Title not available (Why is that?)
• Proving fairness and implementation correctness of a microkernel scheduler
• Inference rules for proving the equivalence of recursive procedures
• The higher-order-logic Formath
• Formal proofs for theoretical properties of Newton's method
• Formal verification of a generic framework to synthesize SAT-provers
• Hammering towards QED
• A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA)
• Formal verification of the VAMP floating point unit
• Formalization of fixed-point arithmetic in HOL
• Code-carrying theories
• Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers
• Efficient execution in an automated reasoning environment
• Quantitative verification of Kalman filters
• Verification of Year 2000 conversion rules using the ACL2 theorem prover
• Rough Diamond: An Extension of Equivalence-Based Rewriting
• A formalization of the Smith normal form in higher-order logic
• A System for Computing and Reasoning in Algebraic Topology
• Proof assistance for real-time systems using an interactive theorem prover
• Verification of FM9801: An out-of-order microprocessor model with speculative execution, exceptions, and program-modifying capability
• Automated and scalable verification of integer multipliers
• The ACL2 Sedan Theorem Proving System
• TIP: Tools for Inductive Provers
• Title not available (Why is that?)
• The Imandra Automated Reasoning System (System Description)
• An experiment concerning mathematical proofs on computers with French undergraduate students
• Coverset Induction with Partiality and Subsorts: A Powerlist Case Study
• Incorporating quotation and evaluation into Church's type theory
• A parameterized floating-point formalizaton in HOL Light
• Extending Coq with Imperative Features and Its Application to SAT Verification
• Formal Methods in Computer-Aided Design
• Automated formal analysis and verification: an overview
• An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model
• Formalization of Euler-Lagrange equation set based on variational calculus in HOL light
• The correctness of the fast Fourier transform: A structured proof in ACL2
• Satisfiability modulo bounded checking
• Title not available (Why is that?)
• Deadlock in packet switching networks
• Varieties of regular semigroups with uniquely defined inversion
• Separation logic-based verification atop a binary-compatible filesystem model
• Mechanical Verification of SAT Refutations with Extended Resolution
• Scaling up livelock verification for network-on-chip routing algorithms
• Implementing and reasoning about hash-consed data structures in Coq
• Certifying properties of an efficient functional program for computing Gröbner bases
• Separation Logic Adapted for Proofs by Rewriting

This page was built for software: ACL2