References:
References Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification Kami: A Framework for (RISC-V)HW Verification
Reference: The Coq Proof Assistant Isabelle advantages over Coq: From Benjamin Pierce notion of equality is extensional; it eliminates a lot of low-level tedium in proofs of involves equality. a much better story about variable binding; formalizing sth that involves binding variables. nominal data type package. Coq = Gallina + Tactics Gallina Core of the Coq: Gallina, a functional programming language; Heart of Gallina: typed lambda calculus.
References: Higher order logic (HOL) Isar - Intelligible semi-automated reasoning. Concrete Semantics Video: Haskell for imperative programmers Video: Math 220, Pepperdine.edu Structured Proof Language. Arithmetic Expressions: Concrete Abstract 5 N 5 (constants) x V “x” (variables) x + y Plus (V “x”) (V “y”) 2 + (z + 3) Plus (N 2) (Plus (V “z”) (N 3))
References: 一文读懂基于SCADE模型的形式化方法 More
References: jfmc’s Z3 Playground Z3 wiki Z3 is a state-of-the-art theorem prover from Microsoft Research. It can be used to check the satisfiability of logical formulas over one or more theories. More
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?