Luca Negrini
Logo

Luca Negrini

static-analysis  abstract-interpretation  teaching

Teaching Through Practice: Advanced Static Analysis with LiSA

Authors: L. Negrini, V. Arceri, L. Olivieri, A. Cortesi, P. Ferrara
Formal Methods Teaching (FMTea 2024)
Milan, Italy, September 10, 2024
Workshop paper

Abstract

Nowadays, ready-to-use libraries and code generation are often used to streamline and speed up the software development process. The resulting programs are thus a collection of different modules that cooperate: proving their safety and reliability is increasingly complex, requiring sound formal techniques, such as static program analysis. However, while teaching static analysis to master’s or PhD students, the predominant focus on theoretical concepts often leaves limited space for students to engage with the practical aspects of implementing static analyses and is limited to developing elementary ones. In this paper, we show how the infrastructure offered by LiSA can be exploited to learn how to implement advanced static analyses, such as string and relational numerical analyses, just focusing on their distinctive aspects. This would help to narrow the gap between theoretical and practical contents in static analysis courses, bringing the learning experience beyond the rudimentary implementation of static analyses to more sophisticated applications.

Manuscript: PDF
Conference talk:Talk @ FMTea 2024
Associated project: LiSA
Conference page: Link
Springer page: Link