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


  • “Quantitative Analysis of Probabilistic Models of Software Product Lines with Statistical Model Checking” @ FMSPLE 2015
  • “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]
  • “A White Box Perspective on Behavioural Adaptation” @ Software, Services, and Systems 2015 [PDF]
  • “Constraint Design Rewriting” @ SCP 2015 [draft,pdf]
  • “Can we efficiently verify concurrent programs under RMMs in Maude?” @ WRLA 2014 [draft]
  • “Programming and Verifying Component Ensembles” @ FPS 2014 [draft]
  • “Reputation-based Cooperation in the Clouds” @ IFIP TM 2014 [draft]
  • “A Computational Field Framework for Volunteer Clouds” @ SEAMS 2014 [draft]
  • “Modelling and Analyzing Adaptive Self-Assembly Strategies with Maude” @ SCP 2014 [draft]
  • full list or check dblpgoogle scholarmicrosoft academicscopusorcidciteseerisi


  • “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]
  • “State Space C-Reductions for Concurrent Systems in Rewriting Logic” @ GRAPHITE 2013 [slides]
  • “Adaptable Transition Systems” @ ASCENS Meeting 2013 [slides]
  • “A White-box Perspective on Self-Adaptation and Self-Awareness” @ AWASS 2012 [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
  • 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.