email Admissions
en
Menu
email

Static Program Analysis

Course description

Static program analysis is about analyzing software code to learn about its properties without executing it. This course covers both the foundations and practical aspects of automated program analysis. We begin by exploring how mathematical formalisms can be used to reason about program execution. We then study the theory of abstract interpretation, which captures the essence of a broad range of program analyses. During laboratories, students will design and implement analysis tools to find bugs and verify properties of software.

Keywords

  • Semantics of computer programs
  • Static program analysis
  • Abstract interpretation

Prerequisite

Software formal analysis and design (ACF).

Bibliography

  • Tutorial on Static Inference of Numeric Invariants by Abstract Interpretation, by Antoine Miné, 2017.

Biography

Benjamin Farinier is an Associate Professor (Maître de Conférences) at the University of Rennes, in the EPICURE research team. He is primarily interested in the formal verification of safety and security properties, from low-level binary code to high-level specifications.