CloSE - Cloud Solving Engine
Persone
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.