The overall objective of the LMV team is to advance the reliability and security of reactive embedded systems running in the Internet of Things (IoT) ecosystem. We aim to ensure that the software involved satisfies critical properties by leveraging language design and formal methods. To achieve this, we rely on the team’s skills in two areas: 

  • semantics of programming languages and program verification
  • rewriting systems and system verification

The Internet of Things (IoT) is a vast network of components connected to the physical world by means of sensors/actuators and interconnected through the Internet. It makes connected objects new actors of the internet. Billions of components are now connected in this way. The application domains open to this new technology are numerous, including health, transport, environment, smart cities, precision agriculture and industry. The systems we are interested in are reactive or interactive systems, i.e. systems that interact with their environment and whose programs react continuously to the signals and events to which they have access. Moreover, the software we consider is embedded in systems with limited resources: this introduces specific challenges.
To carry out this programme, the LMV team relies on collaborations at the local, regional, national and international levels with universities, public institutions and companies. The team is also strongly involved in training by and for research: many students participate in our work. 

LMV members participate to the following working groups: CLAP, LVP, YODA (GDR-GPL) and MFS (GDR-Sécurité).