PV1 Frama-Cframework providing abstractions for C code analysis

Platform/framework for the analysis of C code

Application domain/field

Type of tool


Expected input


.c file with ACSL annotations.

Expected output

Depends on the plugin that is used.


It has many different types of plugins that do different kind of analyses such as WP (deductive verification), E-ACSL (runtime verification), PathCrawler (test case generator) and EVA (value analysis based on abstract interpretation). It uses the specification language ACSL. Some plugins support a subset of ACSL.


It can be run from the command-line or via its graphical user interface. Some plugins are meant to be used via the command-line, not via the GUI.


Related papers

Last publication date

12 July 2021

ProVerB specific

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