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)

• 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
• 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
• TIP: Tools for Inductive Provers
• The Imandra Automated Reasoning System (System Description)
• An experiment concerning mathematical proofs on computers with French undergraduate students
• 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
• A system for computing and reasoning in algebraic topology
• 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
• Scaling up livelock verification for network-on-chip routing algorithms
• Implementing and reasoning about hash-consed data structures in Coq
• Coverset induction with partiality and subsorts: a powerlist case study
• Formalizing simplicial topology in Isabelle/HOL and Coq
• Proving with ACL2 the correctness of simplicial sets in the Kenzo system
• Applying ACL2 to the formalization of algebraic topology: simplicial polynomials
• Certifying properties of an efficient functional program for computing Gröbner bases
• Formalization of a normalization theorem in simplicial topology
• Teaching semantics with a proof assistant: no more LSD trip proofs
• Intelligent computer mathematics. 16th symposium, Calculemus 2009, 8th international conference, MKM 2009, held as part of CICM 2009, Grand Bend, Canada, July 6--12, 2009. Proceedings
• Formalization of transform methods using HOL Light
• The formalization of discrete Fourier transform in HOL
• Translation of resolution proofs into short first-order proofs without choice axioms
• Logic Based Program Synthesis and Transformation
• A verified common lisp implementation of Buchberger's algorithm in ACL2
• Inductive proof search modulo
• An elementary proof of the group law for elliptic curves
• Proof assistants: history, ideas and future
• From LCF to Isabelle/HOL
• Pollack-inconsistency
• Formalization of geometric algebra in HOL Light
• Efficient, verified checking of propositional proofs
• Using abstract stobjs in ACL2 to compute matrix normal forms
• Gauge integral
• Separation logic adapted for proofs by rewriting
• Mechanical verification of SAT refutations with extended resolution
• Agent-oriented modeling of the dynamics of biological organisms
• Reasoning about algebraic data types with abstractions
• Modelling algebraic structures and morphisms in ACL2
• The ACL2 Sedan theorem proving system
• Title not available (Why is that?)
• Title not available (Why is that?)
• ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System
• Ordinals in HOL: transfinite arithmetic up to (and beyond) \(\omega _{1}\)
• Inductive theorem proving based on tree grammars
• The rewriting logic semantics project: a progress report
• A complete proof system for propositional projection temporal logic
• The rewriting logic semantics project: a progress report
• On the fine-structure of regular algebra
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• The rewriting logic semantics project
• A rewriting logic approach to operational semantics
• Proof-Pattern Recognition and Lemma Discovery in ACL2
• Automating Induction with an SMT Solver
• The Reflective Milawa Theorem Prover Is Sound
• Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals
• Title not available (Why is that?)
• Title not available (Why is that?)
• Mizar: State-of-the-art and Beyond
• Transforming Programs into Recursive Functions
• A Brief Overview of HOL4
• A heuristic prover for real inequalities
• Verification Condition Generation Via Theorem Proving
• Function extraction
• Proof pearl: a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks
• Proof pearl: a formal proof of Higman's lemma in ACL2
• Theorem Proving in Higher Order Logics
• Theorem Proving in Higher Order Logics
• Towards a unified theory of operational and axiomatic semantics
• From hoare logic to matching logic reachability
• Meta Reasoning in ACL2
• Termination Analysis with Calling Context Graphs
• Title not available (Why is that?)
• Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
• A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7^™ Processor
• Combining Coq and Gappa for Certifying Floating-Point Programs
• A functional formalization of on chip communications
• Rewriting with equivalence relations in ACL2
• Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18--21, 2008. Proceedings
• Efficiently checking propositional refutations in HOL theorem provers
• Integrating external deduction tools with ACL2
• Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning
• Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets
• Partial functions in ACL2
• Programs from proofs using classical dependent choice
• Structured theory development for a mechanized logic

This page was built for software: ACL2