Our main focus is software. We are looking for methods to ensure the correction of software. To do this, we study their semantic models, their correct construction through refinement techniques, their verification through proof or state exploration techniques (model-checking), their architectures and evolutions over time.

Complex systems that involve the interaction of various physical or software components, important data, time constraints, robustness and quality requirements are difficult to model and develop.

We tackle these difficulties through different themes that revolve around the models. The study of the models is then declined according to different facets in order to cover the different layers of abstractions that constitute a system (software) :

• The services and components that interact in the system
• Analysis of heterogeneous systems
• System architecture and evolution
• Various semantic models (e. g. logical, state, component, service, discrete event, probabilistic, time-delayed, etc.) and associated verification techniques

• Correct software components
• Multiformalism and multifaceted system analysis
• Software architecture
• Probabilistic models, competition semantics, associated verification tools

In relation to these themes, the skills of the team members allow us to explore in particular :

• models for services, components and global architecture ;
• methods of verification by evidence, state exploration and testing.
• reactive, competitive, embedded and information systems.