Sono stati resi noti i vincitori del Turing Award per il 2007: Edmund M. Clarke, E. Allen Emerson e Joseph Sifakis hanno vinto il cosiddetto Nobel dell’informatica per il loro lavoro sui metodi formali di verifica del design e dei requisiti di un sistema (hardware o software che sia). Il loro contributo in particolare ha consentito di sviluppare in modo pratico il metodo noto come Model Checking: attraverso la modellazione di un sistema concorrente in termini di formule di logica temporale, è possibile valutarne la bontà del funzionamento, ovvero è possibile determinare in modo automatico se il sistema rispetta una data specifica. I concetti chiave sono una modellazione attraverso un linguaggio che consenta di rappresentare stati temporali concorrenti, da cui è possibile derivare un albero temporale degli stati (i cui cammini di attraversamento rappresentano tutte i possibili stati in cui il sistema si verrà a trovare) e una logica temporale, detta Computational Tree Logic (CTL), che consenta di verificare delle proprietà del sistema stesso. L’applicazione pratica del Model Checking ha riscontrato successo soprattutto nel campo dell’hardware e limitatamente anche per il software (sono ad esempio note le esperienze di Nasa, Microsoft e Bell Labs).

Trovo questa notizia degna di essere menzionata per tre motivi: intanto i Turing Award sono rilevanti per chiunque si occupi di informatica, sia teorica che pratica, e poi per una volta questo premio dà un senso al termine science in Computer Science. Infine, vale la pena di ricordare che questi metodi spostano di fatto il problema dal sistema in sé verso il modello: sebbene in ambiti limitati la cosa calzi a pennello, è pur vero che la verifica formale avviene sul modello e quindi chi si occupa di verificare il modello stesso? Detto ciò, ben lungi da me sminuire i meriti di Clarke, Emerson e Sifakis.