Saddek Bensalem

Professor at the University Joseph Fourier.

and CEA-Leti ("En Délégation" : 2010-11 et 2011-12).

Distributed and Complex Systems group, Verimag Laboratory

Member of CRI ("Centre de Recherche Intégrative") and ARTIST2 Network of Excellence on Embedded Systems Design.


Phone : (+33) 04 56 52 03 71

Mailing adress : VERIMAG Centre Équation - 2, avenue de Vignate 38610 GIÈRES

Research interests

My interests are in the study of embedded systems, formal specification and verification, algorithmic verification techniques, complex systems, real-time systems, automata and logics. My work has been on the topic of automatic formal verification of systems that have unbounded numbers of states. I have pioneered development of techniques that combine the complementary strengths of deductive and algorithmic methods. I have made significant research contributions on several aspects of this problem. I developed the theory of property-preserving abstraction and relationship to compositional verification, automatic invariant discovery, predicate abstraction and a verification method for parametrized systems. All these techniques are employed in the tool InVeSt developed in collaboration with Yassine Lakhnech and Sam Owre from the SRI. Currently, I collaborate with Joseph Sifakis (Turing Award 2007) on the research project "Rigorous Embedded Systems Design - BIP framework". This research project addresses the end-to-end design for large-scale heterogeneous embedded systems. The key motivations are facilitation of the design of advanced heterogeneous embedded systems with distributed SW. At the same time it can provide a rigorous design flow with performance analysis & validation for multiple programming models to target hardware architectures including multiple heterogeneous smart subsystems and components. The aim of the project is to provide a design flows with the following key objectives:

  • 1. Efficient handling of heterogeneity.
  • 2. Handling of extra-functional constraints.
  • 3. Verification at design time.
  • 5. Adaptability for optimization of extra-functional constraints at run-time.
  • Futur Events

  • "FM 2012" 18th International Symposium on Formal Methods
  • "DATE 2012" Design, Automation& Test in Europe
  • "RV 2012" 3rd International Conference on Runtime Verification.
  • "FMOODS & FORTE 2012" IFIP International Conference on Formal Techniques for Distributed Systems
  • "ESWEEK 2012" Embedded Systems Week
  • "WRLA 2012" 9TH International Workshop on Rewriting Logic and its Applications
  • "M2A2 2012" The 4th IEEE International Workshop on Multicore and Multithreaded Architectures and Algorithms
  • " FMSAS 2012" First International Workshop on Formal Methods for Self-Adaptive Systems (FMSAS 2012)
  • " VECoS 2012" 6th International Workshop on Verification and Evaluation of Computer and Communication Systems
  • Administrative activities

  • Coordinator of the "Master Franco-Hellénique"
  • Member of the "Conseil des Etudes et de la Vie Universitaire (CEVU) de l'Uniservité Joseph Fourier".
  • Member of the "Commission des moyens du CEVU de l'Uniservité Joseph Fourier".
  • Member of the "Commission des finances de l'Université Joseph Fourier".