Experience Report: Teaching Code Analysis and Verification Using Frama-C

Salwa Souaf; Frédéric Loulergue

doi:10.4204/EPTCS.349.5

Experience Report: Teaching Code Analysis and Verification Using Frama-C

Logic in Computer Science 2021-11-17 v1

Authors: Salwa Souaf , Frédéric Loulergue

View on arXiv ↗ PDF ↗ DOI ↗

Abstract

Formal methods provide systematic and rigorous techniques for software development. We strongly believe that they must be taught in computer science curricula. In this paper we present the pedagogic rationale and the concrete implementation of two courses on the use of formal methods, sharing some material. These courses promote the usage of formal verification to ensure safety and security of software, exemplified in the domain of the Internet of Things.

Keywords

formal verification software engineering education program analysis

Cite

@article{arxiv.2111.08208,
  title  = {Experience Report: Teaching Code Analysis and Verification Using Frama-C},
  author = {Salwa Souaf and Frédéric Loulergue},
  journal= {arXiv preprint arXiv:2111.08208},
  year   = {2021}
}

Comments

In Proceedings AppFM 2021, arXiv:2111.07538

Related papers

View all related →