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

Roberta Calegari

Adjunct professor

Research fellow

keywords: logic programming, distributed systems, service-oriented architectures, pervasive systems, intelligent systems, LPaaS,

Andrea Colledan

PhD Student

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

Ugo Dal Lago

Full Professor

keywords: Programming Languages, Quantum Computation, Cryptography, Logic in Computer Science

Maurizio Gabbrielli

Full Professor

keywords: Programming languages, Constraint programming, Artificial Intelligence

Saverio Giallorenzo

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

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

Roberto Gorrieri

Full Professor

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

Pietro Lami

PhD Student

Teaching tutor

keywords: Operational semantics, Reversible languages, Formal Methods, Reversible Computing

Ivan Lanese

Associate Professor

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

Cosimo Laneve

Full Professor

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

Simone Martini

Full Professor

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

Ghulam Mustafa

PhD Student

Andrea Omicini

Full Professor

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

Luca Padovani

Full Professor

keywords: Type systems, Behavioral types, Concurrent and distributed systems, Process algebras, Formal software verification

Claudio Sacerdoti Coen

Associate Professor

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

Mirko Viroli

Full Professor

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