TY - GEN
T1 - Teaching Frama-C for Cybersecurity
AU - Signoles, Julien
N1 - Publisher Copyright:
© The Author(s), under exclusive license to Springer Nature Switzerland AG 2026.
PY - 2026/1/1
Y1 - 2026/1/1
N2 - This article presents my feedback on introducing Frama-C for cybersecurity in several engineering and master’s level university courses. It consists of a single lecture and a single lab session. Frama-C is an open source platform providing C code analyzers based on formal methods. The course focuses on its three main techniques provided through dedicated analyzers, namely deductive verification with Wp, abstract interpretation with Eva, and runtime annotation verification with E-ACSL. The aim of the course is to introduce students to these formal techniques, emphasizing their practical aspects in cybersecurity.
AB - This article presents my feedback on introducing Frama-C for cybersecurity in several engineering and master’s level university courses. It consists of a single lecture and a single lab session. Frama-C is an open source platform providing C code analyzers based on formal methods. The course focuses on its three main techniques provided through dedicated analyzers, namely deductive verification with Wp, abstract interpretation with Eva, and runtime annotation verification with E-ACSL. The aim of the course is to introduce students to these formal techniques, emphasizing their practical aspects in cybersecurity.
UR - https://www.scopus.com/pages/publications/105040636736
U2 - 10.1007/978-3-032-26743-6_7
DO - 10.1007/978-3-032-26743-6_7
M3 - Conference contribution
AN - SCOPUS:105040636736
SN - 9783032267429
T3 - Lecture Notes in Computer Science
SP - 111
EP - 126
BT - Formal Methods Teaching - 7th Formal Methods Teaching Workshop, FMTea 2026, Proceedings
A2 - Carvalho, Gustavo
A2 - Kobayashi, Tsutomu
PB - Springer Science and Business Media Deutschland GmbH
T2 - 7th Formal Methods Teaching Workshop, FMTea 2026
Y2 - 19 May 2026 through 19 May 2026
ER -