scientific article; zbMATH DE number 193479
From MaRDI portal
Publication:4040283
zbMATH Open0655.68117MaRDI QIDQ4040283FDOQ4040283
Authors: Robert S. Boyer, J Strother Moore 
Publication date: 5 June 1993
Title of this publication is not available (Why is that?)
Recommendations
Research exposition (monographs, survey articles) pertaining to computer science (68-02) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Mechanization of proofs and logical operations (03B35)
Cited In (75)
- Title not available (Why is that?)
- New uses of linear arithmetic in automated theorem proving by induction
- On the comparison of HOL and Boyer-Moore for formal hardware verification
- A proof of the nonrestoring division algorithm and its implementation on an ALU
- A temporal logic for real-time partial ordering with named transactions
- Automatic derivation of the irrationality of \(e\)
- Simulation Refinement for Concurrency Verification
- Title not available (Why is that?)
- Simulation refinement for concurrency verification
- Ordered rewriting and confluence
- Wait-free concurrent memory management by Create and Read until Deletion (CaRuD)
- Theories for mechanical proofs of imperative programs
- Hybrid interactive theorem proving using nuprl and HOL
- Specification and verification of concurrent programs through refinements
- A formalization of powerlist algebra in ACL2
- On extensibility of proof checkers
- Using induction and rewriting to verify and complete parameterized specifications
- Techniques of computable set theory with applications to proof verification
- Incorporating quotation and evaluation into Church's type theory
- A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
- A theorem prover for a computational logic
- A verification system for concurrent programs based on the Boyer-Moore prover
- Proof pearl: a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks
- A Ramsey theorem in Boyer-Moore logic
- An integrated approach to high integrity software verification
- Mathematical induction in Otter-lambda
- Invariants for the construction of a handshake register
- Bounded delay for a free address
- On Shostak's decision procedure for combinations of theories
- A PVS Theory for Term Rewriting Systems
- Rewriting with equivalence relations in ACL2
- N. G. de Bruijn's contribution to the formalization of mathematics
- Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem
- Convergence: integrating termination and abort-freedom
- The addition of bounded quantification and partial functions to a computational logic and its theorem prover
- Lazy techniques for fully expansive theorem proving
- Foundations of a theorem prover for functional and mathematical uses
- A formalization of the Knuth-Bendix(-Huet) critical pair theorem
- ACL2s: ``the ACL2 sedan
- The reflective Milawa theorem prover is sound (down to the machine code that runs it)
- A verified runtime for a verified theorem prover
- Mechanical verification on strategies
- A verified common lisp implementation of Buchberger's algorithm in ACL2
- Annotations in formal specifications and proofs
- Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
- Operating system verification---an overview
- Proof assistants: history, ideas and future
- SAD as a mathematical assistant -- how should we go from here to there?
- Structuring and automating hardware proofs in a higher-order theorem- proving environment
- Proving Ramsey's theory by the cover set induction: A case and comparision study.
- The application of automated reasoning to questions in mathematics and logic
- An ACL2 Tutorial
- Algebraic models of microprocessors architecture and organisation
- Verifying a distributed list system: A case history
- Partial and nested recursive function definitions in higher-order logic
- Machine checked proofs of the design of a fault-tolerant circuit
- An overview of the Tecton proof system
- A mechanical proof of Segall's PIF algorithm
- Middle-out reasoning for synthesis and induction
- Using hints to increase the effectiveness of an automated reasoning program: Case studies
- Wait-free linearization with a mechanical proof
- Coq and hardware verification: a case study
- Verification by Parallelization of Parametric Code
- Fundamentals of logic and computation. With practical automated reasoning and verification
- Proof movie -- a proof with the Boyer-Moore prover
- Herbrand's theorem and term induction
- Inductive benchmarks for automated reasoning
- Milestones from the Pure Lisp Theorem Prover to ACL2
- Theory extension in ACL2(r)
- A two-level formal verification methodology using HOL and COSMOS
- Mechanically checked proofs of kernel specifications
- Mechanically verifying safety and liveness properties of delay insensitive circuits
- Getting saturated with induction
- Circuits as streams in Coq: Verification of a sequential multiplier
- An ordinal measure based procedure for termination of functions
Uses Software
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4040283)
