The following pages link to (Q3753927):
Displaying 20 items.
- A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL (Q541222) (← links)
- Automatic verification of a class of systolic circuits (Q1189257) (← links)
- Universal algebra in higher types (Q1199827) (← links)
- Logic, sets, and mathematics (Q1209798) (← links)
- Set theory for verification. I: From foundations to functions (Q1319386) (← links)
- Rule-based induction (Q1334895) (← links)
- Accelerating tableaux proofs using compact representations (Q1334905) (← links)
- Structuring and automating hardware proofs in a higher-order theorem- proving environment (Q1801500) (← links)
- Indentification of inductive properties during verification of synchronous sequential circuits (Q1893131) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Computer assisted reasoning. A Festschrift for Michael J. C. Gordon (Q2655321) (← links)
- The use of \(B\) to specify, design and verify hardware (Q2751751) (← links)
- Coquet: A Coq Library for Verifying Hardware (Q3100217) (← links)
- Computational logic: its origins and applications (Q4559535) (← links)
- Abstraction of hardware construction (Q4645815) (← links)
- Circuits as streams in Coq: Verification of a sequential multiplier (Q4647582) (← links)
- ACKERMANN’S FUNCTION IN ITERATIVE FORM: A PROOF ASSISTANT EXPERIMENT (Q5037519) (← links)
- Proving and rewriting (Q5096184) (← links)
- Verification of asynchronous circuits by BDD-based model checking of Petri nets (Q5096372) (← links)
- A formalised theorem in the partition calculus (Q6073894) (← links)
