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