PV3 SecCchecks user-specified information flow properties of C code

"A prototype program verification tool for proving information flow security of C code."

Application domain/field

Type of tool

Deductive verifier? Auto-active verifier?

Expected input


C file


An automatic verifier (for a subset of C) for SecCSL. SecCSL (Security Concurrent Separation Logic) is used to specify data-dependent information flow security properties of low-level programs. SecC reasons about a program using symbolic execution, similar to Verifast and Viper.


The underlying logic, SecCSL, has been proven sound with Isabelle/HOL.


Related papers

SecCSL: Security Concurrent Separation Logic (CAV 2019)

Last publication date

12 July 2019

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.