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



  • A framework for quantitative modeling and analysis of highly (re)configurable systems [draft]
  • A Holistic Approach for Collaborative Workload Execution in Volunteer Clouds [draft]
  • 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…


  • 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.