swMATH ID: 37554
Software Authors: Letan T
Description: FreeSpec: a compositional reasoning framework for the Coq theorem prover. SpecCert is a framework for specifying and verifying Hardware-based Security Enforcement (HSE) mechanisms against hardware architecture models. HSE mechanisms form a class of security enforcement mechanism such that a set of trusted software components relies on hardware functions to enforce a security policy.
Homepage: https://github.com/lthms/speccert
Dependencies: Coq
Related Software: GitHub; operational; Kami; Rocksalt; Eff; FoCaLiZe; Paco; Coquet; ESC/Java; Spec#; Haskell; Coq
Cited in: 1 Publication

Citations by Year