FreeSpec

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.

References in zbMATH (referenced in 1 article )

Showing result 1 of 1.
Sorted by year (citations)

  1. Letan, Thomas; RĂ©gis-Gianas, Yann; Chifflier, Pierre; Hiet, Guillaume: Modular verification of programs with effects and effects handlers (2021)