Il progetto CONCERTo (CONtrollo e CERTificazione dell'uso delle risorse) è finanziato dal Ministero dell'Istruzione, Università e Ricerca all'interno del programma PRIN (Progetti di Rilevanza Nazionale).

In questo progetto s'intende gettare le fondamenta teoriche per la definizione di strumenti di analisi (essenzialmente statici) finalizzati a garantire proprietà operazionali di programmi legate in particolare all'uso delle risorse, in modelli computazionali sia sequenziali che concorrenti.

Una gestione statica dell'uso delle risorse è di importanza crescente nell'ambito della computazione mobile e distribuita. L'area di ricerca a cui ci riferiamo ha come scopo quello di associare ad un programma una certificazione, che ne garantisca particolari proprietà computazionali, in particolare la quantità di risorse (tempo e spazio, ma non solo) necessarie per la sua esecuzione. Per queste finalità ci baseremo su strumenti e tecniche derivati dalla logica, più specificamente teoria della dimostrazione, e sulla semantica, guardando in particolare alla logica lineare e al lambda calcolo.

La ricerca che noi vogliamo portare avanti è essenzialmente fondazionale, e può essere idealmente suddivisa in due obiettivi principali. Noi vogliamo produrre:

1. Tecniche fondazionali per l'analisi e la verifica di proprietà operazionali di programmi;
2. Teorie computazionali che modellino l'interazione corretta con l'ambiente.

• Descrizione del progetto
• Elenco delle unità di ricerca