Formal methods

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

Roberta Calegari

Adjunct professor

Research fellow

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

foto della persona

Roberto Casadei

Senior assistant professor (fixed-term)

keywords: software engineering, programming paradigms, multi-agent systems, distributed systems, distributed artificial

foto della persona

Ugo Dal Lago

Full Professor

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

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

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

Simone Martini

Full Professor

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

foto della persona

Ghulam Mustafa

PhD Student

foto della persona

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

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,