• Formal Methods
  • Distributed and Concurrent Systems
  • Safety and Security
  • Software Engineering
  • Artificial Intelligence


  • Model Checking (DTU/02246)
  • Introduction to Coordination in Distributed Applications (DTU/02148)
  • Computer Science Modelling (DTU/02141)


  • A framework for quantitative modeling and analysis of highly (re)configurable systems [draft pdf]
  • Aggregation Policies for Tuple Spaces (COORDINATION 2018) [draft pdf]
  • Star-Topology Decoupling in SPIN (SPIN 2018) [draft pdf]
  • Improving availability in distributed tuple spaces via sharing abstractions and replication strategies (PDP 2018) [pdf]
  • A Holistic Approach for Collaborative Workload Execution in Volunteer Clouds (TOMACS 2018) [pdf]
  • Many-to-many Information Flow Policies (COORDINATION 2017) [pdf draft]
  • Asynchronous Distributed Execution Of Fixpoint-Based Computational Fields (LMCS 2017) [pdf]
  • A coordination language for databases (LMCS 2017) [pdf]
  • Statistical Model Checking for Product Lines (ISOLA 2016) [pdf]
  • Microservices: yesterday, today, and tomorrow (PAUSE 2017)  [draft]
  • Information Flow Control for Interaction-Oriented Specifications (Festschrift Meseguer) [pdf draft]
  • AVOCLOUDY: A Simulator of Volunteer Clouds (SPE 2016) [draft pdf]
  • Replicating Data for Better Performances in X10 (Festschrift Nielson & Nielson) [pdf draft]
  • Statistical Analysis of Probabilistic SPL Models with Quantitative Constraints (SPLC 2015) [pdf draft]
  • Replica-based High-Performance Tuple Space Computing (COORDINATION 2015) [draft pdf]
  • Klaim-DB: A Kernel Language for Distributed Databases (COORDINATION 2015) [pdf]
  • A Fixpoint-based Calculus for Graph-shaped Computational Fields (COORDINATION 2015) [draft pdf]
  • full list or check dblpgoogle scholarscopusorcidisi


  • Many-to-Many Information Flow Policies [slides]
  • Aggregate Programming through a Soft Modal Logic [slides]
  • Discretionary Information Flow Control for Choreographies [slides]
  • A Semiring-valued Temporal Logic [slides]
  • Can we efficiently verify concurrent programs under RMMs in Maude?  [slides]
  • Collaborative Task Execution In Volunteer Clouds [slides]
  • more‚Ķ


  • CyberSec4Europe: European H2020 Cybersecurity Competence Network Project
  • QUANTICOL: European FP7 Project on Quantitative Approach to Collective and Adaptive Systems
  • CINA: Italian Compositionality, Interaction, Negotiation, Autonomicity for the future ICT society
  • ASCENS: European FP7 Project on Autonomic Service Component Ensembles
  • SENSORIA: European FP6 Project on Software Engineering for Service-Oriented Computing

Conferences and Journals


Software Tools

  • pSpaces: Programming with Spaces
  • HSF-SPIN: an extension of the Spin model checker with directed model checking algorithms
  • Promela Database: a collection of Promela models for the Spin model checker

Student Projects

  • BSc/MSc projects: contact me or see some project proposals here or here.
  • PhD projects: scholarships from DTU Compute are advertised here.