Laurent Mauborgne

AbsInt, Germany

Laurent Mauborgne

Laurent Mauborgne

AbsInt, Germany

Lecture 5

Applied static analysis: the design of Astrée

Abstract

Astrée is a static analyser based on abstract interpretation, originally developed by Patrick Cousot's team between 2001 and 2009. Since then, it has been further developed and commercialized by AbsInt. One of the key features of Astrée is its ability to analyse large industrial code with soundness guarantees and good precision on safety-critical software. We will explore some of the design choices that made this possible, together with the semantics and some of the abstractions that Astrée uses to adapt to a wide variety of applications. In particular, we will show how Astrée handles asynchronous code, and discuss various challenges raised by the software industry.