In program analysis, there is an idea to use first order logic with theorem prover to “sign” a binary that it is safe with regard to some predefined safety policy.
Eventually it envolved into idea of “proof carrying code”.
A few slides introducing PCC are based on the original PCC paper.
Persistent notes
Alexander Krivutsenko's online journal
-
Custom Search -
More RSS
Powered by