Nicolas Halbwachs - 40 years of static analysis of numerical programs

13:00
Thursday
8
Nov
2018
  • Keynote Speech
Place: 
Organized by: 
The team of the LIG Keynote Speeches: Nicolas Peltier, Renaud Lachaize, Dominique Vaufreydaz
Speaker: 
Nicolas Halbwachs, Verimag, Grenoble
Teams: 

 

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éalisation technique : Antoine Orlandi | Tous droits réservés

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.