The following pages link to NQTHM (Q19570):
Displaying 50 items.
- The reflective Milawa theorem prover is sound (down to the machine code that runs it) (Q286790) (← links)
- Proof pearl: a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks (Q437040) (← links)
- Mechanically certifying formula-based Noetherian induction reasoning (Q507366) (← links)
- Simulation refinement for concurrency verification (Q541209) (← links)
- Orderings for term-rewriting systems (Q593789) (← 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)
- An extension of the Boyer-Moore theorem prover to support first-order quantification (Q688572) (← links)
- N. G. de Bruijn's contribution to the formalization of mathematics (Q740481) (← links)
- Proving Matijasevich's lemma with a default arithmetic strategy (Q809626) (← links)
- A formalization of powerlist algebra in ACL2 (Q846164) (← links)
- Ordinal arithmetic: Algorithms and mechanization (Q851144) (← links)
- Analysis of a biphase mark protocol with Uppaal and PVS (Q855013) (← links)
- Toward automating the discovery of decreasing measures (Q861690) (← 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)
- Verifying a signature architecture: a comparative case study (Q877156) (← links)
- A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures (Q877828) (← links)
- Term rewriting and beyond -- theorem proving in Isabelle (Q909488) (← links)
- Rewriting with equivalence relations in ACL2 (Q928668) (← links)
- A mechanical analysis of program verification strategies (Q928673) (← links)
- A functional formalization of on chip communications (Q931433) (← 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 selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction (Q1075050) (← links)
- The addition of bounded quantification and partial functions to a computational logic and its theorem prover (Q1107510) (← links)
- The verified incremental design of a distributed spanning tree algorithm: Extended abstract (Q1125687) (← links)
- Mechanizing structural induction. I: Formal system (Q1134540) (← links)
- Mechanizing structural induction. II: Strategies (Q1134541) (← links)
- Context induction: A proof principle for behavioural abstractions and algebraic implementations (Q1179807) (← links)
- A semi-algorithm for algebraic implementation proofs (Q1199928) (← 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)
- Nonconstructive computational mathematics (Q1272604) (← links)
- Superposition theorem proving for abelian groups represented as integer modules (Q1275020) (← 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)
- Set theory for verification. I: From foundations to functions (Q1319386) (← links)
- IMPS: An interactive mathematical proof system (Q1319391) (← links)
- Deductive and inductive synthesis of equational programs (Q1322836) (← links)
- Introduction to the OBDD algorithm for the ATP community (Q1332638) (← links)
- Annotations in formal specifications and proofs (Q1334901) (← links)
- A mechanically verified incremental garbage collector (Q1336946) (← links)
- On proving the termination of algorithms by machine (Q1341666) (← links)
