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.