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

Links

Last commit date

11 May 2022

Related papers

https://doi.org/10.1007/978-3-030-17462-0_22 (TACAS 2019)

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.