Ricerca di contatti, progetti,
corsi e pubblicazioni

CloSE - Cloud Solving Engine

Persone

 

Pezzè M.

(Responsabile)

Aquino A.

(Collaboratore)

Chen M.

(Collaboratore)

Abstract

La verifica automatica di programmi è stata studiata fino dagli anni settanta e ha prodotto ottimi risultati. Le principali tecniche di prova usano risolutori automatici di vincoli per valutare la verità delle congetture derivate durante l'analisi.  Purtroppo nonostante i grossi passi avanti degli ultimi anni i risolutori automatici di vincoli sono ancora lenti e trattano solo sottoinsiemi di teorie. Questo progetto intende mettere a punto tecniche che permettano di salvare le prove effettuate per vari programmi e utilizzare queste informazioni per risolvere nuovi vincoli. L'uso di tecniche di ricerca rapida come quelle basate su Map Reduce e Hadoop accoppiate a tecniche di astrazione e memorizzazione dei vincoli dovrebbero permettere nel tempo di identificare velocemente vincoli già provati e permettere di concentrare il lavoro dei risolutori automatici su pochi nuovi vincoli che a loro volta potranno andare a popolare gli insiemi di vincoli già risolti.

Informazioni aggiuntive

Acronimo
CloSE
Data d'inizio
01.10.2013
Data di fine
30.09.2017
Durata
48 Mesi
Enti finanziatori
SNSF
Stato
Concluso
Categoria
Swiss National Science Foundation / Project Funding / Mathematics, Natural and Engineering Sciences (Division II)