FreeSpec 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 Cited by 4 Authors 1 Chifflier, Pierre 1 Hiet, Guillaume 1 Letan, Thomas 1 Régis-Gianas, Yann Cited in 1 Serial 1 Formal Aspects of Computing Cited in 1 Field 1 Computer science (68-XX) Citations by Year