Nicolas Halbwachs is "directeur de recherche émérite" at Verimag Laboratory. He was director of Verimag from 2007 to 2015. His main research contributions concern program analysis and real-time system design. In program analysis, he designed the "linear relation analysis", an abstract interpretation for discovering invariant linear inequalities among numerical variables of a program. In real-time system design, he defined, with Paul Caspi, the synchronous data-flow language Lustre, for programming embedded control software. He studied also the verification of synchronous programs by model-checking and abstract interpretation. Lustre is an industrial success-story, as it became the core language of the worldwide used toolset Scade.
Résumé :
Static analysis of programs consists in extracting guaranteed properties about all executions of a program without executing it. Such properties are useful in compilation, verification, optimization and evaluation of programs. Abstract interpretation, introduced by Patrick and Radhia Cousot in the late seventies, is the theoretical framework of static analysis. In this talk, we will focus on static analysis of numerical properties, like variable boundedness or more general invariant relations between numerical variables. During the last decades, such analyses have been widely studied, in view of finding a compromise between the expressiveness of considered properties and the cost of the analysis. We will try to summarise these works together with their main applications.
Informations
- Gricad Vidéos
- 1 janvier 2021 00:00
- Conférences
- Français
