L’excellente conférence internationale de sécurité informatique NoSuchCon 2014 Rolf Rolles a présenté des méthodes et des exemples d’application de la synthèse de programme à partir d’une spécification pour reconstituer le fonctionnement d’un automate matériel ou logiciel. La théorie au cœur de ces méthodes répond au nom de problème SMT (Satisfiability Modulo Theories), et elle permet, si je puis me permettre un raccourci très sommaire, de calculer un programme à partir de la spécification (…)