• Formal Methods: Model Checking, Verification, Temporal/Graph/Rewriting Logics.
  • Programming Languages: Semantics, Process Algebras, Graph Transformation.
  • Distributed and Concurrent Systems: Global Computing, Services, Coordination.
  • Software Engineering: Autonomic Computing, Cloud Computing, Security.
  • Artificial Intelligence: Heuristic Search, Adaptive Systems, Self-* Systems.


  • Model Checking (DTU/2016/2015/2014, IMT/2015/2014/2013)
  • Introduction to Coordination in Distributed Applications (DTU/2017/2016)
  • Computer Science Modelling (DTU/2107)
  • Programming in C++ (DTU/2016/2015)
  • Reliable Software Systems (DTU/MSc)
  • Old: Writing and Presenting Science and Engineering (DTU/2015), Advanced Analysis Techniques (DTU/2015), Introduction to Formal Verification @ GSSI/2013, Algorithms @ IMT Lucca (Fall 2013Spring 2013), Specification and Verification with Maude @ IMT Lucca (2013, 2010), A white-box perspective on Adaptation @ AWASS 2012 (2012), more…


  • Asynchronous Distributed Execution Of Fixpoint-Based Computational Fields [draft]
  • Statistical Model Checking for Product Lines [draft]
  • A coordination language for databases [draft]
  • Microservices: yesterday, today, and tomorrow [draft]
  • Discretionary Information Flow Control for Interaction-Oriented Specifications [draft]
  • Replicating Data for Better Performances in X10 [draft]
  • Statistical Analysis of Probabilistic SPL Models with Quantitative Constraints (SPLC 2015) [draft]
  • AVOCLOUDY: A Simulator of Volunteer Clouds (SPE) [draft pdf]
  • 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]
  • The SCEL Language (Software Engineering for Collective Autonomic Systems) [draft pdf]
  • Perspectives on Adaptation (Software Engineering for Collective Autonomic Systems) [draft pdf]
  • A White Box Perspective on Behavioural Adaptation (Software, Services, and Systems) [pdf]
  • Constraint Design Rewriting (Science of Computer Programming) [pdf draft]
  • Can we efficiently verify concurrent programs under RMMs in Maude? (WRLA 2014) [draft]
  • Programming and Verifying Component Ensembles (From Programs to Systems) [draft]
  • Reputation-based Cooperation in the Clouds (IFIP TM 2014) [draft]
  • A Computational Field Framework for Collaborative Volunteer Clouds (SEAMS 2014) [draft]
  • Modelling and analyzing self-assembling strategies (Science of Computer Programming) [pdf draft]
  • full list or check dblpgoogle scholarmicrosoft academicscopusorcidciteseerisi


  • Aggregate Programming through a Soft Modal Logic @ LMU [slides]
  • Discretionary Information Flow Control for Choreographies @ BETTY Meeting 2015 [slides]
  • A Semiring-valued Temporal Logic @ IDEA4CPS [slides]
  • Can we efficiently verify concurrent programs under RMMs in Maude? @ WRLA 2014 [slides]
  • Collaborative Task Execution In Volunteer Clouds @ CINA Meeting 2014 [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

  • C-Reducer: Automatic c-reduction of object based modules for the Maude system
  • MESSI: Maude Ensemble Strategies Simulator and Inquirer
  • HSF-SPIN: an extension of the Spin model checker with directed model checking algorithms
  • Promela Database: a collection 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.
  • Industry BSc/MSc/PhD projects: see (e.g. this IoT project).