Project

Back to overview

CloSE: Cloud Solving Engine

English title CloSE: Cloud Solving Engine
Applicant Pezzè Mauro
Number 149997
Funding scheme Project funding (Div. I-III)
Research institution Istituto del Software (SI) Facoltà di scienze informatiche
Institution of higher education Università della Svizzera italiana - USI
Main discipline Information Technology
Start/End 01.10.2013 - 30.09.2017
Approved amount 431'630.00
Show all

Keywords (4)

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

Lay Summary (Italian)

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 
Direct link to Lay Summary Last update: 02.12.2013

Responsible applicant and co-applicants

Employees

Publications

Publication
Heuristically matching solution spaces of arithmetic formulas to efficiently reuse solutions
Andrea Aquino Giovanni Denaro Mauro Pezze (2017), Heuristically matching solution spaces of arithmetic formulas to efficiently reuse solutions, in Proceedings of the International Conference on Software Engineering, Buenos AiresIEEE, New York.
Reusing constraint proofs in program analysis
Andrea Aquino Francesco A. Bianchi Meixian Chen Giovanni Denaro Mauro Pezze (2015), Reusing constraint proofs in program analysis, in Proceedings of the International Symposium on Software Testing and Analysis, BaltimoreACM, New York.
Scalable program analysis through proof caching
Andea Aquino (2015), Scalable program analysis through proof caching, in Proceedings of the International Symposium on Software Testing and Analysis, BaltimoreACM, New York.
Reusing constraint proofs for scalable program analysis
Chen Meixian (2014), Reusing constraint proofs for scalable program analysis, in Proceedings of the 2014 International Symposium on Software Testing and Analysis, San JoseASCM, New York.

Collaboration

Group / person Country
Types of collaboration
Politecnico di Milano Italy (Europe)
- in-depth/constructive exchanges on approaches, methods or results
- Publication
University of Milano Bicocca Italy (Europe)
- in-depth/constructive exchanges on approaches, methods or results
- Publication

Scientific events

Active participation

Title Type of contribution Title of article or contribution Date Place Persons involved
International Confer- ence on Software Engineering Talk given at a conference Heuristically matching solution spaces of arithmetic formulas to efficiently reuse solutions 20.05.2017 Buenos Aires, Argentina Pezzè Mauro; Aquino Andrea;
ACM International Symposium on Software Testing and Analysis Talk given at a conference Scalable program analysis through proof caching 14.07.2015 Baltimore, United States of America Aquino Andrea;
ACM International Symposium on Software Testing and Analysis Talk given at a conference Reusing constraint proofs in program analysis 14.07.2015 Baltimore, United States of America Aquino Andrea;
International Symposium on Software Testing and Analysis Talk given at a conference Reusing constraint proofs for scalable program analysis 21.07.2014 San Jose, United States of America Chen Meixian;


Knowledge transfer events

Active participation

Title Type of contribution Date Place Persons involved
Oracle Cloud Day Talk 09.11.2016 Brugg, Switzerland Pezzè Mauro;
PROUD: Predicting Cloud Failures in Real Time Talk 21.02.2016 Las Vegas, United States of America Pezzè Mauro;


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 conjecturesgenerated 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 verificationtechniques, 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 alreadysolved 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.
-