Software Engineering and Security

The Department's research in this area covers a rich variety of topics, including: automated static analysis, cryptography, formal language definitions, formal methods, formal security models, formal software verification, logic and verification, malware and its mitigation, massively parallel systems, network security, parallel programming languages, security protocols, security services, semantics, social aspects of security and privacy, software and application security, software architectures, software functional properties, software reverse engineering, software system models, software verification and validation, system description languages, trust frameworks, Unified Modeling Language (UML), web protocol security.


pdf Brochure di presentazione dell'area  (pdf,  it, 254 KB)
pdf Presentazione Research Day 2017  (pdf,  it, 5121 KB)
Matteo Cristani
Assistant Professor
Mila Dalla Preda
Temporary Assistant Professor
Alessandra Di Pierro
Associate Professor
Roberto Giacobazzi
Full Professor
Isabella Mastroeni
Associate Professor
Massimo Merro
Full Professor
Roberto Segala
Full Professor
Nicola Fausto Spoto
Associate Professor
Luca Vigano'
Research Assistants
Topic People Description
Formal methods and theory of security standard compliant  ACM 2012
Formal methods and theory of security Matteo Cristani
Roberto Segala
Luca Vigano'
Development of formal, and possibly automated, methods for the analysis of the security of software systems
Formal methods for security analysis of cyber-physical systems Massimo Merro
Development of formal, and possibly automated, methods for the security analysis of cyber-physical systems and IoT systems
Probabilistic Analysis of Security Alessandra Di Pierro
Roberto Segala
Static analysis of approximate security properties via Probabilistic Abstract Interpretation
Code protection Mila Dalla Preda
Roberto Giacobazzi
Isabella Mastroeni
Luca Vigano'
Development of formal techniques and tools for the protection of software.
Network security standard compliant  ACM 2012
Network security Matteo Cristani
Luca Vigano'
Development of techniques and tools for the security of computer networks
Software and application security standard compliant  ACM 2012
Formal software and application security Mila Dalla Preda
Roberto Giacobazzi
Isabella Mastroeni
Development of models and analyses, based on abstract interpretation, for the security application verification and for security properties enforcement.
Software and application security Luca Vigano'
Development of security methodologies and technologies for the security of software systems and Internet applications
Software creation and management standard compliant  ACM 2012
Code synthesis Mila Dalla Preda
Roberto Giacobazzi
Isabella Mastroeni
Study and development of techniques for the synthesis of code (or code transformers) from the specification of semantic code properties.
Software creation and management Luca Vigano'
Study and development of formal and semi-formal methodologies and technologies for the creation and management of software systems
Software Verification Luca Vigano'
Decision procedures for satisfiability modulo theories and their application to check program properties; invariant generation by theorem proving; interpolating theorem proving; abstraction refinement for either model checking or static analysis by theorem proving
Software organization and properties standard compliant  ACM 2012
Static Analysis Mila Dalla Preda
Roberto Giacobazzi
Isabella Mastroeni
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.
Quantitative static analysis Alessandra Di Pierro
Study of formal methods for quantitative analysis of programs. Extension of classical program analysis techniques (data-flow, control-flow, abstract interpretation,type systems)to probabilistic and speculative analysis for program optimisation and transformation.
Verification of wireless network protocols Massimo Merro
Semantics-based and model-checking techniques for the verification of wireless network protocols
Gruppi di ricerca
Name Description URL
K.Re.Art.I. Rappresentazione della conoscenza tramite tecniche di IJntelligenza Artificiale
Logica Logica in matematica ed informatica.
QUILAB Quantum Informatics Laboratory
REGIS: Research Group in Information Security Studio e sviluppo di metodologie formali per l'analisi, l'ottimizzazione, la certificazione, la robustezza e la sicurezza di sistemi software complessi
Title Managers Sponsors Starting date Duration (months)
Abstract interpretation based analysis of Scripting Languages - Joint Projects 2014 Isabella Mastroeni Maxfone s.r.l. 12/1/14 24
Analisi e sviluppo di tecniche di analisi semantica di codice Java industriale Nicola Fausto Spoto Julia s.r.l. 7/1/15 24
Static analysis methods for the static derivation Roberto Giacobazzi Julia s.r.l. 6/5/13 16
IDACOP - Interpretation-based design and measurement of code-protecting transformations - Joint Projects 2014 Roberto Giacobazzi Irdeto Canada Corporation 11/1/14 24
La messa a punto di Strumenti innovativi per la ricerca semantica Nicola Fausto Spoto Corvallis S.p.A. 7/1/15 24
Computer Engineering for Industry 4.0 Franco Fummi MIUR 1/1/18 60
Security Horizons Luca Vigano' MIUR 2/1/13 36
Static Analysis for Multithreading - Joint Project 2011 Massimo Merro Julia s.r.l. 1/1/13 30
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
Development of Semantic Analysis Techniques for Java Code Nicola Fausto Spoto Julia s.r.l. 7/1/17 18
Theorem proving algorithms for program analysis: interpolants, models, and termination (PRIN 2012 non finanziato) Maria Paola Bonacina 2/18/13 36
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 36


Research facilities