Document ID: /fineweb-2-swissfilter-quality_10-filterrobots/filtered/01256.jsonl.gz/489

Motore di risoluzione nel Cloud
In sintesi
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.
soggetto e obiettivo
L'obiettivo ambizioso di questo progetto è la produzione di un sistema per la ricerca automatica di vincoli già risolti in passato che permetta di estendere tecniche di verifica automatica a programmi di grandi dimensioni.
Il progetto deve affrontare numerosi problemi che comprendono la definizione di un formato opportuno per la memorizzazione e la ricerca rapida di vincoli, la definizione di algoritmi di ricerca altamente paralleli, la normalizzazione di vincoli.
Contesto socio-scientifico
Provare formalmente la correttezza di un programma software darebbe maggiori garanzie sull'uso del software. Questo progetto potrebbe migliorare in modo eclatante l'affidabilità di tanti prodotti che fanno affidamento sul software.
parole chiave
Constraint solving, Symbolic execution, Automated verification, Program correctness