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