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)

• A complete proof system for propositional projection temporal logic
• The rewriting logic semantics project: a progress report
• Computer Solutions of Problems in Inverse Semigroups
• 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?)
• 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
• Meta Reasoning in ACL2
• Correct Hardware Design and Verification Methods
• 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
• Multi-Prover Verification of Floating-Point Programs
• Programs from proofs using classical dependent choice
• Structured theory development for a mechanized logic
• Theorem Proving in Higher Order Logics
• Automatic verification of reduction techniques in higher order logic
• Title not available (Why is that?)
• Artificial Intelligence and Symbolic Computation
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• Title not available (Why is that?)
• Title not available (Why is that?)
• HOL Light QE
• The Rewriting Logic Semantics Project: A Progress Report
• Recycling proof patterns in Coq: case studies
• Towards a Unified Theory of Operational and Axiomatic Semantics
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• Reasoning About Incompletely Defined Programs
• Formalized linear algebra over Elementary Divisor Rings in Coq
• Iterated ultrapowers for the masses
• Operating system verification---an overview
• Certifying algorithms
• Mechanizing Mathematical Reasoning
• A two-valued logic for properties of strict functional programs allowing partial functions
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• Formalization of Bernstein polynomials and applications to global optimization
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Formalization of real analysis: a survey of proof assistants and libraries
• A formal proof of the deadline driven scheduler in PPTL axiomatic system
• Ordinal arithmetic: Algorithms and mechanization
• Formal Proof of a Wave Equation Resolution Scheme: The Method Error
• An even closer integration of linear arithmetic into inductive theorem proving
• Nonstandard analysis in ACL2
• On the role of formalization in computational mathematics
• Operational Reasoning for Concurrent Caml Programs and Weak Memory Models
• Partial and nested recursive function definitions in higher-order logic
• Formalizing on chip communications in a functional style
• Tools and algorithms for the construction and analysis of systems. 17th international conference, TACAS 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011, Saarbrücken, Germany, March 26 -- April 3, 2011. Proceedings
• From Hoare Logic to Matching Logic Reachability
• Proceedings of the 7th workshop on user interfaces for theorem provers (UITP 2006), Seattle, WA, USA, August 21, 2006
• A Verified Runtime for a Verified Theorem Prover
• Point-Free, Set-Free Concrete Linear Algebra
• Hammer for Coq: automation for dependent type theory
• Construction and analysis of ground models and their refinements as a foundation for validating computer-based systems
• Coquelicot: a user-friendly library of real analysis for Coq
• Proof Pearl: Wellfounded Induction on the Ordinals Up to ε 0
• 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

This page was built for software: ACL2