SPARK: Vous ne pouvez simplement pas écrire de meilleur code

SPARK est un langage de programmation conçu pour la vérification formelle et l'analyse statique. L'une des principales caractéristiques du langage SPARK est la capacité d'exprimer des contrats. c'est-à-dire des propriétés comportementales qui doivent être implémentées correctement par le développeur et peuvent être automatiquement vérifiées par des d'outils.

Dans cet exposé, je vais faire une brève introduction au langage, présenter quelques projets où il est utilisé (sécurité et aérospatiale), ainsi que des astuces pour commencer à utiliser SPARK vous-même.