Frama-C
Frama-C is a popular open-source toolset for analysis and verification of C programs, largely used for teaching, experimental research, and industrial applications.
Security DSLs provided by the Tool
Name
Description
Security Checks provided by the Tool
Name
Description
SecureFlow is a security-oriented plug-in aimed at verifying that the values of private memory locations cannot influence the values of public locations, i.e. that there are no information leaks in the program.
DeadlockF is a plugin for detection of deadlocks in multithreaded C programs with mutexes.
The Evolved Value Analysis plug-in computes variation domains for variables.