Static analysis by abstract interpretation of concurrent programs
type: Dataset
description: This report presents the bulk of my research work from the completion of my PhD, in late 2004, until the present day. The overall aim of my research is the development of mathematically sound and practically efficient methods to check the correctness of computer software. Efficiency is achieved using approximations, while soundness is guaranteed by employing over-approximations of program behaviors. My research is grounded in the theory of abstract interpretation, a powerful mathematical framework facilitating the development, use, comparison, and composition of approximations in a sound way. I am mainly interested in developing new reusable abstraction components (so called abstract domains) that can be readily implemented, and in using them to develop static analyzers, which are computer programs able to check automatically the safety of software. While my early research was focused on inferring the values of variables in sequential programs, my current interest and latest results concern the analysis of concurrent programs, hence the title of this report. The first two chapters of this report constitute an introduction. The first chapter is an informal introduction to the problem at hand, existing solutions, their strengths and their shortcomings. The second chapter presents prior mathematical and formal tools on which our work is based, including some notions of abstract interpretation, a description of existing abstract domains and their application to the static analysis of sequential programs. It also recalls some results I obtained during my PhD and that will be useful in the rest of the report. The subsequent chapters describe the work I performed after completing my PhD. The third chapter is devoted to aspects of static analyzers that are specific to concurrent programs. This topic of personal research has led to the construction of a generic analysis method for concurrent programs, parametrized by the choice of abstract domains. The method is based on a n…
issued: 2026-05-08T06:47:18.257281
language: en
modified: 2026-05-08T06:47:18.257286
contact point: Organization
  fn: CCSD
keyword: abstract-interpretation
keyword: analyse-statique
keyword: concurrents-programs
keyword: domaines-numeriques
keyword: embedded-programs
keyword: habilitation-a-diriger-des-recherches
keyword: infoeu-reposemanticsother
keyword: infoinfo-escomputer-science-csembedded-systems
keyword: infoinfo-flcomputer-science-csformal-languages-and-automata-theory-csfl
keyword: infoinfo-pfcomputer-science-csperformance-cspf
keyword: interpretation-abstraite
keyword: numeric-domains
keyword: programmes-concurrents
keyword: programmes-embarques
keyword: safety
keyword: static-analysis
keyword: surete-de-fonctionnement
keyword: verification
landing page: https://theses.hal.science/tel-00903447

Static analysis by abstract interpretation of concurrent programs
type: Distribution
format: HTML
issued: 2026-05-08T06:47:18.284343
modified: 2026-05-08T06:47:18.238676
access URL: https://theses.hal.science/tel-00903447

test_moissonnage_selune
type: Agent