Le Turing Award est assorti d'un prix de 250.000 dollars, au financement duquel participent des entreprises comme Intel ou Google ainsi qu'un certain nombre d'organismes de recherche américains.
« Le Model Checking est une méthode algorithmique qui permet de vérifier qu'un système logiciel ou matériel satisfait à des exigences données (de sécurité ou de sûreté par exemple) », explique le CNRS dans un communiqué. Aujourd'hui, il serait largement utilisé dans les industries du matériel et du logiciel informatique pour vérifier l'efficacité de puces, de protocoles de communication, de pilotes logiciels, de systèmes embarqués ou d'algorithmes de sécurité.
« Cette technologie est aujourd'hui utilisée dans l'industrie des circuits intégrés afin de concevoir des systèmes complexes dont on peut garantir la conformité aux spécifications initiales. L'impact industriel du Model Checking devrait être encore plus significatif dans les années à venir notamment en ce qui concerne la vérification des processeurs et des systèmes critiques embarqués », explique encore le CNRS.
