The following pages link to (Q4040283):
Displaying 50 items.
- The reflective Milawa theorem prover is sound (down to the machine code that runs it) (Q286790) (← links)
- Invariants for the construction of a handshake register (Q293438) (← links)
- Proof pearl: a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks (Q437040) (← links)
- Simulation refinement for concurrency verification (Q541209) (← links)
- A formalization of the Knuth-Bendix(-Huet) critical pair theorem (Q616850) (← links)
- Using induction and rewriting to verify and complete parameterized specifications (Q672051) (← links)
- On the comparison of HOL and Boyer-Moore for formal hardware verification (Q685100) (← links)
- N. G. de Bruijn's contribution to the formalization of mathematics (Q740481) (← links)
- A formalization of powerlist algebra in ACL2 (Q846164) (← links)
- An integrated approach to high integrity software verification (Q861714) (← links)
- Mathematical induction in Otter-lambda (Q861715) (← links)
- SAD as a mathematical assistant -- how should we go from here to there? (Q865654) (← links)
- Rewriting with equivalence relations in ACL2 (Q928668) (← links)
- Partial and nested recursive function definitions in higher-order logic (Q972425) (← links)
- A verified common lisp implementation of Buchberger's algorithm in ACL2 (Q1034553) (← links)
- Proof assistants: history, ideas and future (Q1040001) (← links)
- Operating system verification---an overview (Q1040002) (← links)
- A verification system for concurrent programs based on the Boyer-Moore prover (Q1203115) (← links)
- Machine checked proofs of the design of a fault-tolerant circuit (Q1203129) (← links)
- Theories for mechanical proofs of imperative programs (Q1267030) (← links)
- Lazy techniques for fully expansive theorem proving (Q1309245) (← links)
- A proof of the nonrestoring division algorithm and its implementation on an ALU (Q1314510) (← links)
- A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol (Q1318283) (← links)
- Annotations in formal specifications and proofs (Q1334901) (← links)
- An overview of the Tecton proof system (Q1341710) (← links)
- Proving Ramsey's theory by the cover set induction: A case and comparision study. (Q1353938) (← links)
- The application of automated reasoning to questions in mathematics and logic (Q1354049) (← links)
- Verifying a distributed list system: A case history (Q1355754) (← links)
- A mechanical proof of Segall's PIF algorithm (Q1362774) (← links)
- A temporal logic for real-time partial ordering with named transactions (Q1391307) (← links)
- Convergence: integrating termination and abort-freedom (Q1647960) (← links)
- Incorporating quotation and evaluation into Church's type theory (Q1753993) (← links)
- Structuring and automating hardware proofs in a higher-order theorem- proving environment (Q1801500) (← links)
- Algebraic models of microprocessors architecture and organisation (Q1815999) (← links)
- Mechanical verification on strategies (Q1896369) (← links)
- Bounded delay for a free address (Q1901690) (← links)
- A Ramsey theorem in Boyer-Moore logic (Q1904403) (← links)
- New uses of linear arithmetic in automated theorem proving by induction (Q1915133) (← links)
- Middle-out reasoning for synthesis and induction (Q1915136) (← links)
- Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem (Q1915139) (← links)
- Using hints to increase the effectiveness of an automated reasoning program: Case studies (Q1923820) (← links)
- Inductive benchmarks for automated reasoning (Q2128807) (← links)
- Fundamentals of logic and computation. With practical automated reasoning and verification (Q2240968) (← links)
- Milestones from the Pure Lisp Theorem Prover to ACL2 (Q2280212) (← links)
- Specification and verification of concurrent programs through refinements (Q2351261) (← links)
- Proof movie -- a proof with the Boyer-Moore prover (Q2366695) (← links)
- Herbrand's theorem and term induction (Q2491080) (← links)
- Theory extension in ACL2(r) (Q2642461) (← links)
- ACL2s: ``the ACL2 sedan'' (Q2867932) (← links)
- A Verified Runtime for a Verified Theorem Prover (Q3088011) (← links)
