Il ‘fratello maggiore’ dell’intelligenza artificiale

Non ci sono solo l’intelligenza artificiale e il machine learning, ma l’informatica ha anche altre frontiere su cui gli scienziati sono impegnati. Una di queste riguarda i “metodi formali” che consentono di verificare l’efficacia di sistemi, come circuiti elettronici o programmi software, prima ancora della loro realizzazione.

“La verifica dei sistemi è fondamentale per quelli molto critici, come sono quelli per veicoli a guida autonoma, i sistemi di controllo del traffico aereo o ferroviario e gli impianti di produzione di energia” spiega il professor Angelo Montanari, dell’Università di Udine. È stato proprio lui, assieme al collega di ateneo Gabriele Puppis e a Tiziano Villa dell'Università di Verona, ad aver coordinato la scuola estiva, organizzata dai due atenei, che per l’intera settimana ha impegnato nel Cism di Udine una settantina di ricercatori (due terzi in presenza e un terzo da remoto) provenienti da una molteplicità di nazioni: Italia, Germania, Belgio, Olanda, Regno Unito, Polonia, Austria, Francia, Islanda, Romania, Cina, India, Russia, Ungheria, Danimarca, Malta e Israele.

“I metodi formali – continua Montanari - costruiscono dei modelli dei sistemi e consentono di verificare in modo rigoroso, ovvero matematico, se essi soddisfano o meno un certo insieme di proprietà desiderate prima di costruire effettivamente il sistema. Numerosi strumenti software, basati sui metodi formali studiati dai ricercatori, sono stati sviluppati e vengono correntemente utilizzati per eseguire in modo automatico tali verifiche”.

Il lavoro fatto a Udine ha cercato di affrontare questioni poste già negli Anni ’50 da Alonzo Church, uno dei padri riconosciuti dell'informatica, tra cui quella di poter produrre sistemi-programmi corretti per costruzione.

Questo è possibile, ad esempio, nella sintesi di controllori di piano e di strumenti che consentono di monitorare il comportamento di un sistema, riconoscendo per tempo l'insorgenza di situazioni che, in assenza di interventi appropriati, causerebbero malfunzionamenti o guasti del sistema stesso.

Udine, così, si conferma un punto di riferimento internazionale in questo settore dell’informatica al pari dei più celebri e blasonati atenei. Già nel 1978 il Cism aveva ospitato la quinta edizione di una delle conferenze internazionali più importanti di informatica teorica (International Colloquium on Automata, Languages and Programming), organizzata dall'Associazione europea di informatica teorica, e nel 2018 l’ateneo friulano ha organizzato il convegno annuale europeo dell'Associazione di logica simbolica (Logic Colloquium).