Typestates Specification and Verification in Frama-C

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.