• Reliable Software Systems (DTU/MSc)
  • Model Checking (DTU/2015, IMT/2015/2014/2013)
  • Presentation and Analytical Techniques (DTU/2015)
  • Introduction to Coordination in Distributed Applications (DTU/2016)
  • Programming in C++ (DTU/2016, DTU/2015)
  • Writing and Presenting Science and Engineering (DTU/2016)
  • Old: 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…

Research Interests

  • Formal Methods, Model Checking, Verification, Logics, Graph Transformation, Rewriting Logic
  • Software Engineering, Global Computing, Service-Oriented Computing, Autonomic Computing
  • Artificial Intelligence, Adaptive Systems, Self-* Systems


  • 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]
  • Quantitative Analysis of Probabilistic Models of Software Product Lines with Statistical Model Checking (FMSPLE 2015) [pdf]
  • The SCEL Language: Design, Implementation, Verification (Software Engineering for Collective Autonomic Systems 2015) [pdf]
  • Reconciling White-Box and Black-Box Perspectives on Behavioral Self-adaptation (Software Engineering for Collective Autonomic Systems 2015) [pdf]
  • Tools for Ensemble Design and Runtime (Software Engineering for Collective Autonomic Systems 2015) [pdf]
  • A White Box Perspective on Behavioural Adaptation (Software, Services, and Systems 2015) [pdf]
  • Constraint Design Rewriting (Science of Computer Programming 2015) [pdf draft]
  • Can we efficiently verify concurrent programs under RMMs in Maude? (WRLA 2014) [draft]
  • Programming and Verifying Component Ensembles, (From Programs to Systems – The Systems Perspective in Computing 2014) [draft]
  • Reputation-based Cooperation in the Clouds (IFIP TM 2014) [draft]
  • A Computational Field Framework for Collaborative Task Execution in Volunteer Clouds (SEAMS 2014) [draft]
  • Modelling and analyzing adaptive self-assembling strategies with Maude (Science of Computer Programming 2014) [pdf draft]
  • full list or check dblpgoogle scholarmicrosoft academicscopusorcidciteseerisi



  • 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
  • more…

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


Complete CV can be found here.