scientific article; zbMATH DE number 193479
From MaRDI portal
Publication:4040283
Recommendations
Cited in
(78)- A verified common lisp implementation of Buchberger's algorithm in ACL2
- Proof assistants: history, ideas and future
- Operating system verification---an overview
- The addition of bounded quantification and partial functions to a computational logic and its theorem prover
- A verification system for concurrent programs based on the Boyer-Moore prover
- Machine checked proofs of the design of a fault-tolerant circuit
- Theories for mechanical proofs of imperative programs
- Lazy techniques for fully expansive theorem proving
- A proof of the nonrestoring division algorithm and its implementation on an ALU
- A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
- Annotations in formal specifications and proofs
- An overview of the Tecton proof system
- 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
- Verifying a distributed list system: A case history
- A mechanical proof of Segall's PIF algorithm
- A temporal logic for real-time partial ordering with named transactions
- Convergence: integrating termination and abort-freedom
- Incorporating quotation and evaluation into Church's type theory
- Structuring and automating hardware proofs in a higher-order theorem- proving environment
- Algebraic models of microprocessors architecture and organisation
- Mechanical verification on strategies
- Bounded delay for a free address
- A Ramsey theorem in Boyer-Moore logic
- New uses of linear arithmetic in automated theorem proving by induction
- Middle-out reasoning for synthesis and induction
- Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem
- Using hints to increase the effectiveness of an automated reasoning program: Case studies
- Inductive benchmarks for automated reasoning
- Fundamentals of logic and computation. With practical automated reasoning and verification
- Milestones from the Pure Lisp Theorem Prover to ACL2
- Specification and verification of concurrent programs through refinements
- Proof movie -- a proof with the Boyer-Moore prover
- Herbrand's theorem and term induction
- Theory extension in ACL2(r)
- The reflective Milawa theorem prover is sound (down to the machine code that runs it)
- ACL2s: ``the ACL2 sedan
- Invariants for the construction of a handshake register
- A verified runtime for a verified theorem prover
- An ACL2 Tutorial
- scientific article; zbMATH DE number 5539366 (Why is no real title available?)
- Foundations of a theorem prover for functional and mathematical uses
- Proof pearl: a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks
- On Shostak's decision procedure for combinations of theories
- Circuits as streams in Coq: verification of a sequential multiplier
- Techniques of computable set theory with applications to proof verification
- Wait-free linearization with a mechanical proof
- Wait-free concurrent memory management by create and read until deletion (CaRuD)
- A PVS theory for term rewriting systems
- Hybrid interactive theorem proving using Nuprl and HOL
- Simulation Refinement for Concurrency Verification
- Simulation refinement for concurrency verification
- Verification by Parallelization of Parametric Code
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- An ordinal measure based procedure for termination of functions
- Automatic derivation of the irrationality of e
- On extensibility of proof checkers
- Getting saturated with induction
- A formalization of the Knuth-Bendix(-Huet) critical pair theorem
- Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
- A theorem prover for a computational logic
- Ordered rewriting and confluence
- Mechanically checked proofs of kernel specifications
- A two-level formal verification methodology using HOL and COSMOS
- Mechanically verifying safety and liveness properties of delay insensitive circuits
- Coq and hardware verification: a case study
- Using induction and rewriting to verify and complete parameterized specifications
- On the comparison of HOL and Boyer-Moore for formal hardware verification
- A unified view of induction reasoning for first-order logic
- Rewriting and inductive reasoning
- Induction in saturation
- N. G. de Bruijn's contribution to the formalization of mathematics
- A formalization of powerlist algebra in ACL2
- An integrated approach to high integrity software verification
- Mathematical induction in Otter-lambda
- SAD as a mathematical assistant -- how should we go from here to there?
- Rewriting with equivalence relations in ACL2
- Partial and nested recursive function definitions in higher-order logic
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)
