PV4 ⊧ IFC-CEGARchecks if a program is safe with respect to variables marked secret
- Security verification
- Information flow
Type of toolModel checker?
- Set of high-security variables
Format:C-program with annotations indicating the secret variables and the locations at which leaks should be checked.