Formal methods

Formal methods research exploits mathematical techniques for the design, implementation and verification of software systems, usually of high complexity or with particularly stringent quality requirements. This research covers a wide spectrum of activities, ranging from theoretical studies on the fundamental properties of computability and interaction to theorem proving (also interactive, i.e., able to develop formal demonstrations and automatically verifiable through human-machine collaboration), from models of concurrent systems to models with rich mathematical theories with which to specify and verify salient properties of the systems, such as deadlock absence, possibly through automatic or semi-automatic tools.
The group represents a departmental research line articulated in several thematic units each of which has a specific person in charge.

People

foto della persona

Andrea Colledan

PhD Student

Teaching tutor

keywords: Lambda calculus, Quantum programming languages, Operational semantics, Resource verification
foto della persona

Ugo Dal Lago

Full Professor

keywords: Differential Program Semantics, Quantum Computation, Cryptography, Automated Complexity Analysis
foto della persona

Maurizio Gabbrielli

Full Professor

keywords: Programming languages, Constraint programming, Artificial Intelligence
foto della persona

Saverio Giallorenzo

Fixed-term Researcher in Tenure Track L. 79/2022

keywords: Programming Languages, Process Algebras, Session Types, Choreographic Programming, Microservices, Dynamic Adaptability,
foto della persona

Roberto Gorrieri

Full Professor

keywords: Models for the description of concurrent systems, Process algebras and Petri nets, Information-flow security,
foto della persona

Pietro Lami

PhD Student

Teaching tutor

keywords: Operational semantics, Reversible languages, Formal Methods, Reversible Computing
foto della persona

Ivan Lanese

Associate Professor

keywords: Quantum computing, Reversible languages, Multiparty sessions, Service-oriented computing
foto della persona

Cosimo Laneve

Full Professor

keywords: programming languages, static analysis of programs, programming languages semantics, prototype implementations of
foto della persona

Uzma Latif

PhD Student

keywords: Predictive Maintenance, Machine Learning, Artificial Intelligence,Computer Vision, Software Engineering and Formal
foto della persona

Simone Martini

Full Professor

keywords: Programming languages, History and philosophy of computing, Computer science education, Linear logic
foto della persona

Andrea Omicini

Full Professor

keywords: simulation, intelligent agents, multiparadigm languages, self-organising systems, pervasive computing, multiagent
foto della persona

Claudio Sacerdoti Coen

Associate Professor

keywords: Type theory, Interactive theorem proving, Mathematical knowledge management, Lambda-calculus, Programming languages,
foto della persona

Mirko Viroli

Full Professor

keywords: Object-oriented languages, Multiagent systems, Simulation and verification, Coordination, Software engineering,