Ingegneria del Software e Verifica Formale

  1. Home
  2. Ricerca
  3. Aree di ricerca
  4. Ingegneria del Software e Verifica Formale
L’area di ingegneria del software e verifica formale del DI incentra l’attività di ricerca nella realizzazione di metodologie e strumenti innovativi a supporto della progettazione, sviluppo e validazione del software. La ricerca sulla progettazione del software si concentra su architetture smart contracts e blockchain, studiando pattern architetturali solidi e sicuri, e sui fondamenti semantici di sistemi wireless. La verifica del software è investigata secondo molteplici prospettive: (i) analisi statica e interpretazione astratta, anche con riferimento a proprietà (es. intensionali/estensionali) che ne determinano la precisione e allo sviluppo di misure di (im)precisione; (ii) generazione automatizzata di casi di test per rilevare difetti di implementazione e vulnerabilità; (iii) studio di modelli per la progettazione e la verifica formale di sistemi concorrenti, distribuiti e con componenti mobili; e (iv) approcci deduttivi alla verifica automatica del software tramite soddisfacibilità modulo teorie. Queste attività di ricerca sono applicate a molteplici tipologie di sistemi software, inclusi bockchain, smart contracts, REST APIs, smartphone apps, IoT, edge-computing, sistemi ciberfisici, programmi quantistici, software scritti in linguaggi di programmazione dinamici o con molteplici linguaggi di programmazione.
Maria Paola Bonacina
Professore ordinario
Mariano Ceccato
Professore associato
Mila Dalla Preda
Professore associato
Isabella Mastroeni
Professore associato
Massimo Merro
Professore ordinario
Sara Migliorini
Ricercatore a tempo determinato
Michele Pasqua
Ricercatore a tempo determinato
Roberto Segala
Professore ordinario
Nicola Fausto Spoto
Professore associato
Competenze
Argomento Persone Descrizione
Automated static analysis aderente allo standard  ACM 2012
Analisi statica di programmi Mila Dalla Preda
 Isabella Mastroeni
 Michele Pasqua
 Nicola Fausto Spoto
 		Studio di tecniche di analisi statica per linguaggi di programmazione. Inferenza di proprietà della memoria dinamica dei programmi. Inferenza di proprietà di sicurezza per le informazioni manipolate dai programmi.
Formal software verification aderente allo standard  ACM 2012
Verifica formale del software Maria Paola Bonacina
 		Applicazione di procedure di decisione per la soddisfacibilità modulo teorie (SMT) e assegnamenti (SMA) alla verifica dei programmi; generazione di invarianti, generazione di interpolanti di dimostrazioni, e raffinamento di astrazioni (per model checking o analisi statica) mediante dimostrazione automatica di teoremi.
Software creation and management aderente allo standard  ACM 2012
Blockchain e smart contracts Sara Migliorini
 Nicola Fausto Spoto
 		Progettazione di smart contracts e applicazioni basate su blockchain.
Software organization and properties aderente allo standard  ACM 2012
Verifica di protocolli di rete wireless Massimo Merro
 		Tecniche semantiche e di model checking, anche statistico, per la verifica della correttezza di protocolli di reti wireless.
Software testing and debugging aderente allo standard  ACM 2012
Testing del software Mariano Ceccato
 Michele Pasqua
 		Generazione automatica di casi di test per rivelare difetti di implementazione e vulnerabilità in sistemi software come API REST, app per smartphone e smart contracts.
Models of computation aderente allo standard  ACM 2012
Modelli formali della computazione Isabella Mastroeni
 		Studio di tecniche e modelli formali per la caratterizzazione di problemi di analisi  e di safety nin sistemi computazionali di varia natura, come reti neurali e sistemi quantistici.
Modelli per sistemi concorrenti, distribuiti e mobili Massimo Merro
 Michele Pasqua
 		Calcoli di processo per sistemi concorrenti, distribuiti e con mobilità di codice e/o agenti. Più di recente, calcoli di processo per sistemi ciberfisici e sistemi IoT.
Modelli per sistemi ibridi Roberto Segala
 		Studio di modelli per la rappresentazione di sistemi concorrenti che esibiscono comportamenti sia discreti che continui. Uso dei modelli per l'analisi di sistemi distribuiti di controllo.
Modelli stocastici concorrenti Roberto Segala
 		Studio di modelli di concorrenza che includono comportamenti stocastici. Uso di tali modelli per l'analisi di sistemi distribuiti e di protocolli che fanno uso di primitive crittografiche.
Semantics and reasoning aderente allo standard  ACM 2012
Semantica di programmi Mila Dalla Preda
 Isabella Mastroeni
 Michele Pasqua
 Nicola Fausto Spoto
 		Studio di tecniche e modelli semantici per la caratterizzazione di problemi di analisi e di sicurezza nei linguaggi di programmazione.
Semantica di sistemi concorrenti, distribuiti e mobili Massimo Merro
 		Semantica operazionale per linguaggi concorrenti, distribuiti e con mobilità di codice e/o agenti. Tecniche di specifica e di verifica del buon comportamento di tali sistemi.
Gruppi di ricerca
Nome Descrizione URL
ARLette - Laboratorio di Ragionamento Automatico Il gruppo svolge ricerche in Ragionamento Automatico: soddisfacibilità modulo teorie e assegnamenti, procedure di decisione per la soddisfacibilità, dimostrazione di teoremi, costruzione di modelli, riscrittura, e applicazioni.
Big Data Analytics Questo gruppo di ricerca si occupa di tematiche relative alla rappresentazione, gestione e analisi di grandi quantità di dati caratterizzate in particolare dalla dimensione spaziale e temporale.
Blockchain L'attività del gruppo di ricerca riguarda diverse tematiche relative allo sviluppo e all'applicazione della tecnologia blockchain e dell'infrastruttura degli smart contracts.
ForME - Metodi Formali per la Progettazione di Sistemi Ingegneristici Obiettivo del gruppo di ricerca è applicare metodi formali alla modellazione, verifica e sintesi di sistemi ingegneristici. I domini spaziano dai sistemi temporizzati per andare fino ai sistemi ciberfisici non lineari.
INdAM - Unità di Ricerca dell'Università di Verona Raccogliamo qui le attività scientifiche dell'Unità di Ricerca dell'Istituto Nazionale di alta Matematica INdAM presso l'Università di Verona
Intelligenza Artificiale (IA) Il gruppo svolge ricerche in Intelligenza Artificiale: Ragionamento Automatico, Algoritmi di Ricerca, Rappresentazione della Conoscenza, Apprendimento Automatico, Sistemi Multi-Agenti e applicazioni.
SPY
UniVerSE Lab Il gruppo di ricerca del University of Verona Software Engineering (UniVerSE) Lab esplora tecniche all'avanguardia nell'ingegneria del software, con un focus primario sul miglioramento della qualità del software attraverso il testing del software e l'analisi statica di programmi. 
Progetti
Titolo Responsabili Fonte finanziamento Data inizio Durata (mesi) 
VALORLEGNO - Filiera del legno veneto: sistemi avanzati di valorizzazione delle produzioni Daniele Meli Regione del Veneto 01/10/24 31
PRIN PNRR 2022 - Resource Awareness in Programming: Algebra, Rewriting, and Analysis Isabella Mastroeni MUR - Ministero dell'Università e della Ricerca 30/11/23 24
ODIN - AFOSR USA: ABSTRACT INTERPRETATION DRIVEN PROGRAMMING LANGUAGES Mila Dalla Preda AIR FORCE OFFICE OF SCIENTIFIC RESEARCH 15/09/23 60
Studio e formalizzazione di un algoritmo per il calcolo dinamico del prezzo di noleggio dei veicoli Nicola Fausto Spoto Noleggiare s.r.l. 28/07/23 6
Studio e implementazione di una soluzione software in Go verificata per gestione di identità SPID Nicola Fausto Spoto Tradenet Services SRL 20/04/22 8
Audit Colony Nicola Fausto Spoto Audit Colony SRL 01/11/21 12
SafePKT Nicola Fausto Spoto CJDNS SASU 01/07/21 6
Studio e documentazione del framework di sviluppo Cosmos SDK per la programmazione di reti blockchain Nicola Fausto Spoto Commerc.io srl 01/10/20 2
Integrazione del linguaggio Takamaka di programmazione di smart contract in Java con la blockchain Takamaka e sua documentazione per l’utente Nicola Fausto Spoto Ailia SA 16/06/20 6
The SMArt LAbel as a guarantee tool in the WInery-customer trust relationship for Venetian high quality Pgi wines) SMA.LA.WI Roberto Giacobazzi, Mila Dalla Preda Regione Veneto 01/04/19 36
Implementazione di un framework di programmazione in Java per contratti digitali Nicola Fausto Spoto Ailia SA 01/01/19 12
Sviluppo di tecniche di analisi semantica di codice Java Nicola Fausto Spoto Julia s.r.l. 01/07/17 18
JP2016 - Determinazione anticipata di minacce mediante analisi approssimata di similarità in big-code Mila Dalla Preda Joint Projects - assegnato e gestito dal Dipartimento 01/03/17 24
JP2016 - Interpretazione astratta di COBOL Isabella Mastroeni Joint Projects - assegnato e gestito dal Dipartimento 01/03/17 24
Analisi e sviluppo di tecniche di analisi semantica di codice Java industriale Nicola Fausto Spoto Julia s.r.l. 01/07/15 24
La messa a punto di Strumenti innovativi per la ricerca semantica Nicola Fausto Spoto Corvallis S.p.A. 01/07/15 24
Sistema Software di Pianoforte Virtuale su Tablet PC Nicola Fausto Spoto Viscount International S.p.A. 05/02/15 11
Studio e sperimentazione RIA (Rich Internet Application) per soluzioni web e mobile-RIA Nicola Fausto Spoto Add Value S.p.A. 16/01/15 12
JP2014 - TRENDS - Tecnologie e Risorse per sfruttare i documenti InterNet e i Social media Nicola Fausto Spoto Techne Media Agency s.r.l. 01/01/15 24
JP2014 - Progettazione basata sull'interpretazione e misurazione delle trasformazioni del codice di protezione Roberto Giacobazzi Joint Projects - assegnato e gestito dal Dipartimento 01/11/14 24
Theorem proving algorithms for program analysis: interpolants, models, and termination (PRIN 2012 non finanziato) Maria Paola Bonacina 18/02/13 36
Generalizing Truth-Functionality: GeTFun Luca Vigano' Unione Europea 01/01/13 48
Static Analysis for Multithreading - Joint Project 2011 Massimo Merro Julia s.r.l. 01/01/13 30
MoreGAIN - Mismatch smoothing by smart recordering - Joint Projects 2011 Roberto Giacobazzi Energycamente s.r.l. 01/01/12 24

Attività

Aree di ricerca

Gruppi di ricerca

Dottorati di Ricerca

Strutture

Condividi