Projekt

Zurück zur Übersicht

CloSE: Cloud Solving Engine

Titel Englisch CloSE: Cloud Solving Engine
Gesuchsteller/in Pezzè Mauro
Nummer 149997
Förderungsinstrument Projektförderung (Abt. I-III)
Forschungseinrichtung Facoltà di scienze informatiche Università della Svizzera italiana
Hochschule Università della Svizzera italiana - USI
Hauptdisziplin Informatik
Beginn/Ende 01.10.2013 - 30.09.2017
Bewilligter Betrag 431'630.00
Alle Daten anzeigen

Keywords (4)

Program Verification, Symbolic Execution, Parallel MapReduce Style Search, Constraint Solving

Lay Summary (Italienisch)

Lead
La verifica automatica di programmi è stata studiata fino dagli anni settanta e ha prodotto ottimi risultati. Questo progetto metterà 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 permetterà di identificare velocemente vincoli già provati.
Lay summary

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 
Direktlink auf Lay Summary Letzte Aktualisierung: 02.12.2013

Verantw. Gesuchsteller/in und weitere Gesuchstellende

Mitarbeitende

Abstract

The goal of this project is to explore the feasibility of a paradigm shift in the practice of program verification and analysis for industrially relevant programs, by reducing the impact of constraint solving techniques that currently represent a main bottleneck for verification approaches. Program verification and analysis techniques play an important role in software engineering, and have been extensively studied from the early seventies, mostly for proving program properties. They rely on constraint solving to prove the validity of formulas and conjectures generated during the verification. For example, symbolic techniques that are widely used in software engineering require simplifying and proving the validity of path conditions that are constraints on symbolic values, and indicate the conditions on the input values for executing a given set of paths. Both the recent improvements in processing resources and the wider set of applications of these techniques have raised new interests and expectations in program verification and analysis. Despite the spectacular advances in constraint solving techniques and the availability of mature solvers, constraint solving still represents a major bottleneck for program verification. The size of constraints grows quickly with the complexity of the program under analysis and may include hundreds of terms, thus impacting on the performance of the solvers. Many constraints may include terms of different nature, that may require different theories that work selectively on some terms and not others. As a consequence, many promising verification techniques, like many symbolic evaluation approaches, do not scale easily with the program size and the complexity of the terms that can occur in the conditions. This project proposes a new approach to constraint solving that can highly increase the scalability of program verification techniques. Our approach is based on the observation that the same or similar constraints may occur several times when dealing with many programs over time, and the constraints that must be evaluated in a given proof may have been already solved in previous proofs, and thus we can reuse previously saved proofs with a potentially big saving in time and effort. The success of the approach depends on the frequency of occurrence of the same or similar constraints and on the efficiency of the search of previous proofs.