Funded by Commission permanente de coopération franco-québécoise / 63e session / Biennum 2011 et 2012 and through an Équipe Associeé at Inria

Software systems are an integral part of our infrastructure, and our society increasingly depends on its proper functioning: software monitors medical devises, manges our financial assets, and controls power plants. But as consumers take more and more advantage of online services, they are also becoming more concerned about safety: is electronic voting safe, is private information not leaked by the health care provider, are personal data records kept safe by social networking sites or financial institutions, are services such as torrents only uploading data they are supposed to. Establishing safety-related properties of software systems is no longer an academic niche, it is something we as a society must be concerned about because of economic, financial, and social reasons.

The goal of this research network between McGill University and Inria Saclay is to build a common infrastructure for specifying safety properties, proving safety properties and establishing properties about safety policies: from the theory of proofs to the practice of mechanizing the reasoning with and about safety properties. This research contributes to answering questions about how to establish trust by specifying, verifying and validating safety properties about software systems and is an important step towards a general safety infrastructure for software systems.

McGill Team:

Inria Team: