Bertrand Jeannet - Home Page

General Information

Position

I am Chargé de recherche at INRIA (Institut de Recherche en Informatique et Automatique).

I am member of the POP ART of INRIA Rhône-Alpes, located in Grenoble.

Address

Research interests

• Formal verification
• Abstract Interpretation and Static Analysis
• Automatic test/debugging methods
• Probabilistic model-checking

Software and libraries

Programming is part of my activity.

I maintain several libraries:

• OCaml interfaces for various C libraries (CUDD, GMP, LPSOLVE)
• Tools and libraries for static analysis and verification
• Apron: a set of abstract domain libraries sharing the same interface.

I also developped some verification tools:

• NBac: Numerical and Boolean Automaton Checker: a verification tool based on dynamic partitioning to verify safety properties of programs or systems. Connected to the LUSTRE synchronous language and Auto symbolic hybrid automata formalism.
• RAPTURE: Reachability Analysis of Probabilistic Transition systems by sUccsessive Refinements: a verification tool for finite-state probabilistic systems.

I also developped two online interprocedural analyzers:

• Interproc, for sequential programs with numerical variables;
• ConcurInterproc, for concurrent programs with finite-state and numerical variables.

Here a few case studies can be found.

• Interprocedural Shape Analysis with TVLA.
• Analysis of Hybrid Systems with NBac.

Publications

Recent publications

Academic background