Ospite all'USI un premio Turing, il "Nobel" dell'informatica: Joseph Sifakis inaugura l'edizione 2010 di FMCAD

FMCAD (Formal Methods in Computer Aided Design) è una delle principali conferenze internazionali che riguardano la teoria e l'applicazione dei metodi formali (metodi basati su analisi logico-matematiche) per la verifica automatica. L'edizione 2010 di FMCAD sarà tenuta per la prima volta al di fuori degli Stati Uniti: sarà infatti ospitata dalla Facoltà di scienze informatiche dell'USI e si svolgerà dal 20 ottobre al 23 ottobre 2010.

La conferenza sarà inaugurata da una lezione speciale del Dr. Joseph Sifakis. Il Dr. Sifakis ha vinto nel 2007 il Turing Award, l'equivalente del premio Nobel per l'informatica. Attualmente è Direttore della Ricerca del Centro Nazionale Francese per la Ricerca Scientifica, e fondatore del laboratorio VERIMAG, un centro leader nella ricerca nei sistemi embedded. Il titolo della lezione è "Embedded Systems Design, Scientific Challenges and Work Directions".

FMCAD è uno dei principali convegni internazionali per la ricerca accademica e industriale ed ha lo scopo di divulgare e discutere innovazioni riguardo a tecniche, metodi, risultati teorici e strumenti per il ragionamento automatico nell'ambito dei sistemi embedded. I sistemi embedded sono al centro di una vasta gamma di applicazioni nel settore aerospaziale, dei trasporti, delle telecomunicazioni, delle smart card e dei circuiti elettronici di consumo. I sistemi embedded sono composti da un circuito (hardware) ed un programma (software) specificatamente progettati per controllare un particolare dispositivo di controllo, e come tali, sono spesso soggetti a vincoli di elevata affidabilità.

FMCAD sarà presieduta dalla Dr.ssa Natasha Sharygina, prof. alla Facoltà di scienze informatiche, a capo del Laboratorio per la Verifica Formale e la Sicurezza dell'USI. Il laboratorio, istituito nel 2006 dalla stessa professoressa, conduce progetti nella verifica formale automatica, con un particolare interesse per tecniche di Model Checking in ambito hardware e software, sicurezza informatica e procedure di decisione. I membri del laboratorio lavorano sia a metodi teorici che a strumenti pratici che permettono una corretta ed efficiente verifica di sistemi di complessità industriale. Tra i programmi sviluppati nel laboratorio figurano: LoopFrog, uno strumento di verifica basato su analisi statica per la verifica di programmi (per esempio codice C); SecureMobility, un ambiente per la sicurezza informatica nell'ambito di mobile code; OpenSMT, un software efficiente ed open-source che implementa una procedura di decisione di formule logico-matematiche; ProofTransformer, un ambiente di manipolazione e riduzione di dimostrazioni logiche.

• Per il programma dettagliato della conferenza: http://fmcad10.iaik.tugraz.at
• Per una sintesi dell'intervento di Joseph Sifakis http://fmcad10.iaik.tugraz.at/sifakis.html
• Per una biografia di Joseph Sifakis: http://www-verimag.imag.fr/~sifakis/
• Per informazioni sul Laboratorio per la Verifica Formale e la Sicurezza dell'USI: http://www.verify.inf.usi.ch