TY - GEN
T1 - Typestates Specification and Verification in Frama-C
AU - Patte, Sébastien
AU - Prevosto, Virgile
N1 - Publisher Copyright:
© 2025 IEEE.
PY - 2025/1/1
Y1 - 2025/1/1
N2 - Critical software systems need strong safety and security guarantees, since a bug can have very bad consequences. Thus, we need powerful verification techniques, such as formal methods, to assess such systems. Frama-C is an Open-Source platform for formal analysis of C code. It comes with ACSL, a specification language based on function contracts. Recently, a Frama-C plug-in has been developed for stating and verifying Typestates properties. These properties restrict possible operations on objects of a given datatype, depending on their current state. This plug-in instruments the original program with ACSL annotations, in order to use the standard Frama-C analyzers. We propose a formalization for this instrumentation, in order to prove its correctness. To this end, we rely on the Skel metalanguage, the Necrocoq tool, and the Coq proof assistant.
AB - Critical software systems need strong safety and security guarantees, since a bug can have very bad consequences. Thus, we need powerful verification techniques, such as formal methods, to assess such systems. Frama-C is an Open-Source platform for formal analysis of C code. It comes with ACSL, a specification language based on function contracts. Recently, a Frama-C plug-in has been developed for stating and verifying Typestates properties. These properties restrict possible operations on objects of a given datatype, depending on their current state. This plug-in instruments the original program with ACSL annotations, in order to use the standard Frama-C analyzers. We propose a formalization for this instrumentation, in order to prove its correctness. To this end, we rely on the Skel metalanguage, the Necrocoq tool, and the Coq proof assistant.
KW - ACSL
KW - Coq
KW - Formal Methods
KW - Frama-C
KW - Program Analysis
KW - Skel
KW - Skeletal Semantics
KW - Typestates
KW - Verification
UR - https://www.scopus.com/pages/publications/105009071865
U2 - 10.1109/FORMALISE66629.2025.00021
DO - 10.1109/FORMALISE66629.2025.00021
M3 - Conference contribution
AN - SCOPUS:105009071865
T3 - Proceedings - 2025 IEEE/ACM 13th International Conference on Formal Methods in Software Engineering, FormaliSE 2025
SP - 146
EP - 156
BT - Proceedings - 2025 IEEE/ACM 13th International Conference on Formal Methods in Software Engineering, FormaliSE 2025
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 13th IEEE/ACM International Conference on Formal Methods in Software Engineering, FormaliSE 2025
Y2 - 27 April 2025 through 28 April 2025
ER -