Security and Privacy Properties

Point of contact

Virgile Prevosto, CEA List


Historically, formal methods have mostly focused on proving safety properties of critical embedded systems, which were relatively isolated. With the advent of IoT, it becomes more and more important to be able to specify security (i.e. confidentiality, integrity, availability, …) and privacy properties, and to verify that programs are conforming to these specifications. While the underlying analysis techniques are mostly the same, the kind of properties to be investigated can be quite different and warrant further research.

A few references

Related master programs