TY - GEN
T1 - Tame Your Annotations with MetAcsl
T2 - 13th International Conference on Tests and Proofs, TAP 2019, held as part of the 3rd World Congress on Formal Methods, FM 2019
AU - Robles, Virgile
AU - Kosmatov, Nikolai
AU - Prevosto, Virgile
AU - Rilling, Louis
AU - Le Gall, Pascale
N1 - Publisher Copyright:
© 2019, Springer Nature Switzerland AG.
PY - 2019/1/1
Y1 - 2019/1/1
N2 - A common way to specify software properties is to associate a contract to each function, allowing the use of various techniques to assess (e.g. to prove or to test) that the implementation is valid with respect to these contracts. However, in practice, high-level properties are not always easily expressible through function contracts. Furthermore, such properties may span across multiple functions, making the specification task tedious, and its assessment difficult and error-prone, especially on large code bases. To address these issues, we propose a new specification mechanism called meta-properties. Meta-properties are enhanced global invariants specified for a set of functions, capable of expressing predicates on values of variables as well as memory related conditions (such as separation) and read or write access constraints. This paper gives a detailed presentation of meta-properties and their support in a dedicated Frama-C plugin MetAcsl, and shows that they are automatically amenable to both deductive verification and testing. This is demonstrated by applying these techniques on two illustrative case studies.
AB - A common way to specify software properties is to associate a contract to each function, allowing the use of various techniques to assess (e.g. to prove or to test) that the implementation is valid with respect to these contracts. However, in practice, high-level properties are not always easily expressible through function contracts. Furthermore, such properties may span across multiple functions, making the specification task tedious, and its assessment difficult and error-prone, especially on large code bases. To address these issues, we propose a new specification mechanism called meta-properties. Meta-properties are enhanced global invariants specified for a set of functions, capable of expressing predicates on values of variables as well as memory related conditions (such as separation) and read or write access constraints. This paper gives a detailed presentation of meta-properties and their support in a dedicated Frama-C plugin MetAcsl, and shows that they are automatically amenable to both deductive verification and testing. This is demonstrated by applying these techniques on two illustrative case studies.
UR - https://www.scopus.com/pages/publications/85076115512
U2 - 10.1007/978-3-030-31157-5_11
DO - 10.1007/978-3-030-31157-5_11
M3 - Conference contribution
AN - SCOPUS:85076115512
SN - 9783030311568
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 167
EP - 185
BT - Tests and Proofs - 13th International Conference, TAP 2019, held as part of the 3rd World Congress on Formal Methods 2019, Proceedings
A2 - Beyer, Dirk
A2 - Keller, Chantal
PB - Springer
Y2 - 9 October 2019 through 11 October 2019
ER -