Software Engineering and Formal Verification

  1. Home
  2. Research
  3. Research areas
  4. Software Engineering and Formal Verification
The software engineering and formal verification area conducts research on novel methodologies and tools for the design, development, and validation of software systems. Research on software design is concerned with smart contracts and blockchain architectures, focusing on solid and secure architectural patterns, and on semantic foundations of wireless systems. Software verification research adopts multiple perspectives: (i) static analysis and abstract interpretation, also in reference to properties (e.g., intensional/extensional) that affect the analysis’ precision and the design of (im)precision measures; (ii) automatic generation of test cases to reveal implementation defects and vulnerabilities; (iii) investigation of models for the design and the formal verification of concurrent, distributed systems and with mobile components; and (iv) deductive approaches to automated software verification using satisfiability modulo theories. These research activities are applied to a variety of kinds of software systems, including blockchain, smart contracts, REST APIs, smartphone apps, IoT, edge-computing, cyber-physical systems, quantum programs, software developed using dynamic programming languages or with multiple programming languages.
Maria Paola Bonacina
Full Professor
Mariano Ceccato
Associate Professor
Mila Dalla Preda
Associate Professor
Isabella Mastroeni
Associate Professor
Massimo Merro
Full Professor
Sara Migliorini
Temporary Assistant Professor
Michele Pasqua
Temporary Assistant Professor
Roberto Segala
Full Professor
Nicola Fausto Spoto
Associate Professor
Research interests
Topic People Description
Automated static analysis standard compliant  ACM 2012
Static program analysis Mila Dalla Preda
 Isabella Mastroeni
 Michele Pasqua
 Nicola Fausto Spoto
 		Study of techniques for the static analysis of programming languages. Inference of properties of the heap memory used by programs. Inference of security properties for information manipulated by computer programs.
Formal software verification standard compliant  ACM 2012
Formal software verification Maria Paola Bonacina
 		Application of decision procedures for satisfiability modulo theories (SMT) and assignments (SMA) to program verification; invariant generation, interpolation of proofs, and abstraction refinement (for either model checking or static analysis) via automated theorem proving.
Software creation and management standard compliant  ACM 2012
Blockchain and smart contracts Sara Migliorini
 Nicola Fausto Spoto
 		Design of smart contracts and blockchain-based applications.
Software organization and properties standard compliant  ACM 2012
Verification of wireless network protocols Massimo Merro
 		Semantics-based and model-checking techniques for the verification of wireless network protocols.
Software testing and debugging standard compliant  ACM 2012
Software testing Mariano Ceccato
 Michele Pasqua
 		Automatic generation of test cases to reveal implementation defects and vulnerabilities in software systems such as REST APIs, smartphone apps, and smart contracts.
Models of computation standard compliant  ACM 2012
Formal models of computation Isabella Mastroeni
 		Development of formal models for characterizing safety and analysis problems of different computational systems, such as neural networks and quantum systems.
Models for concurrent, distributed, and mobile systems Massimo Merro
 Michele Pasqua
 		Process calculi for concurrent, distributed, and mobile systems. More recently, process calculi for cyber-physical systems and IoT systems.
Models for hybrid systems Roberto Segala
 		Study of models for the representation of concurrent systems exhibiting discrete and continuous behaviors. Use of models for the analysis of distributed control systems.
Concurrent stochastic models Roberto Segala
 		Study of concurrency models that include stochastic behaviors. Use of such models for the analysis of distributed systems and protocols that employ cryptographic primitives.
Semantics and reasoning standard compliant  ACM 2012
Program semantics Mila Dalla Preda
 Isabella Mastroeni
 Michele Pasqua
 Nicola Fausto Spoto
 		Development of semantic models for characterizing security and analysis problems of programming languages
Semantics of concurrent, distributed, and mobile systems Massimo Merro
 		Semantics of concurrent, distributed, and mobile computations. Associated with these semantic theories come specification techniques and verification technologies for assuring the behaviour of systems.
Gruppi di ricerca
Name Description 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
Projects
Title Managers Sponsors Starting date Duration (months)
PRIN PNRR 2022 - Resource Awareness in Programming: Algebra, Rewriting, and Analysis Isabella Mastroeni MUR - Ministero dell'Università e della Ricerca 11/30/23 24
ODIN - AFOSR USA: ABSTRACT INTERPRETATION DRIVEN PROGRAMMING LANGUAGES Mila Dalla Preda AIR FORCE OFFICE OF SCIENTIFIC RESEARCH 9/15/23 60
Study and formalization of an algorithm for the dynamic determination of the renting price of vehicles. Nicola Fausto Spoto Noleggiare s.r.l. 7/28/23 6
Study and implementation of a verified solution in Go for dealing with SPID authentication. Nicola Fausto Spoto Tradenet Services SRL 4/20/22 8
Audit Colony Nicola Fausto Spoto Audit Colony SRL 11/1/21 12
SafePKT Nicola Fausto Spoto CJDNS SASU 7/1/21 6
Study and documentation of the Cosmos SDK for programming blockchains Nicola Fausto Spoto Commerc.io srl 10/1/20 2
Integration between the Takamaka language for smart contracts in Java and the blockchain Takamaka, with user documentation. Nicola Fausto Spoto Ailia SA 6/16/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 4/1/19 36
Implementation of a Java Framework for Smart Contracts Nicola Fausto Spoto Ailia SA 1/1/19 12
Development of Semantic Analysis Techniques for Java Code Nicola Fausto Spoto Julia s.r.l. 7/1/17 18
Big-code early threat detection by approximate similarity analysis Mila Dalla Preda Joint Projects - assegnato e gestito dal Dipartimento 3/1/17 24
Abstract Interpretation of COBOL Isabella Mastroeni Joint Projects - assegnato e gestito dal Dipartimento 3/1/17 24
Analisi e sviluppo di tecniche di analisi semantica di codice Java industriale Nicola Fausto Spoto Julia s.r.l. 7/1/15 24
La messa a punto di Strumenti innovativi per la ricerca semantica Nicola Fausto Spoto Corvallis S.p.A. 7/1/15 24
Sistema Software di Pianoforte Virtuale su Tablet PC Nicola Fausto Spoto Viscount International S.p.A. 2/5/15 11
Studio e sperimentazione RIA (Rich Internet Application) per soluzioni web e mobile-RIA Nicola Fausto Spoto Add Value S.p.A. 1/16/15 12
TRENDS - Technologies and Resources for Exploiting interNet Documents and Social media - Joint Projects 2014 Nicola Fausto Spoto Techne Media Agency s.r.l. 1/1/15 24
Interpretation-based design and measurement of code-protecting transformations Roberto Giacobazzi Joint Projects - assegnato e gestito dal Dipartimento 11/1/14 24
Theorem proving algorithms for program analysis: interpolants, models, and termination (PRIN 2012 non finanziato) Maria Paola Bonacina 2/18/13 36
Generalizing Truth-Functionality: GeTFun Luca Vigano' Unione Europea 1/1/13 48
Static Analysis for Multithreading - Joint Project 2011 Massimo Merro Julia s.r.l. 1/1/13 30
MoreGAIN - Mismatch smoothing by smart recordering - Joint Projects 2011 Roberto Giacobazzi Energycamente s.r.l. 1/1/12 24

Activities

Research facilities

Share