Collection

Tag: hardware-verification

Bounded Model Checking and the Decision to Turn Verification into SAT

Bounded model checking recast finite-depth verification as Boolean satisfiability, using rapidly improving SAT solvers to find deep counterexamples without constructing a global symbolic state representation.

↗

Mike Gordon and HOL: Higher-Order Logic Becomes a Verification Workbench

Mike Gordon’s HOL system adapted the LCF trusted-kernel style to higher-order logic and showed that a general logical formalism could be used for practical hardware specification and mechanized verification.

↗