PV4 MetAcslchecks high-level ACSL requirements by propagating them across the codebase

a Frama-C plugin for specification and verification of high-level properties. Quoting their website:
MetAcsl is a plug-in dedicated to specifying and verifying high-level ACSL requirements (HILARE), that is, properties that are supposed to be checked at many points of the code base under analysis, so that writing the corresponding ACSL annotations manually would be extremely tedious and error-prone.

Expected input


Related papers

MetAcsl: Specification and Verification of High-Level Properties (TACAS 2019)

ProVerB specific

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