• 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


  • Discretionary Information Flow Control for Interaction-Oriented Specifications [draft]
  • Replicating Data for Better Performances in X10 [draft]
  • Statistical Analysis of Probabilistic Software Product Line Models with Quantitative Constraints (SPLC 2015) [draft]
  • AVOCLOUDY: A Simulator of Volunteer Clouds (SPE) [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]
  • 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

Student Projects Proposals (at DTU)

  • Checking and Visualising Flows of Information: Parallel and distributed programs can be specified using high-level interaction-oriented languages (cf. workflows, choreographies, protocols, message sequence charts,…). Such high-level specifications make the analysis of some program properties easier with respect to directly analysing the implementation of the program in some low-level process-oriented language (c.f. Java threads, MPI,…). The goal of the project is to implement a simple flow analysis technique for a basic choreography description language, based on a recently proposed approach [1]. The implementation should be able to check some simple flow policies (specifying which processes can access which data and how) as well as providing a visual graph-based representation of the flows of information.
  • Efficient Data Sharing through Optimistic Data Replication: A simple way of seeing a distributed application is to abstract the underlying computing system (the computer, the cluster, the network, etc.) as set of localities hosting data items (objects, tuples, variables, etc.) and computations (tasks, activities, processes, actors, etc.) that cooperate through local and remote operations on those data. In many applications data needs to be shared among different localities. Data sharing can be implemented using replication mechanisms: the idea is to maintain multiple copies (called replicas) of the same data item on the locations that need to share the data item. The goal of the project is to implement some so-called “optimistic” data replication strategies in a Java-based framework. The idea of such “optimistic” strategies is to allow replicas to temporarily diverge so that localities may have inconsistent views on the shared data. The goal is to sacrifice consistency for the sake of performance, as often done by providers of world-wide services (Amazon, Google,…). The project will be based on recent experiments [1,2] that implement some simple data replication strategies in two Java-based frameworks, namely IBM’s X10 and Klaim.
  • Attribute Based Communication at Work: In a system with concurrent agents (parallel programs, distributed systems, and so on) communication among agents can happen in different ways. For instance, an agent may communicate to another agent (point-to-point communication), a group of agents (multicast communication) or all the agents (broadcast communication). Communication can be tightly or loosely coupled: for instance, the addressed agent(s) may be specified by their unique identifiers (e.g. Alice wants to communicate with Bob and Charlie) or by their properties (e.g. Alice wants to communicate with someone able to providing service X or everyone that subscribed to topic Y). Loosely-coupled communication has been very successful in many applications like web services and publish-subscribe systems. Recently, attribute-based communication has been adopted in some languages (see e.g. [1]) as a form of loosely-coupled communication where an agent can specify its interacting partners as those fulfilling some properties. This communication approach has been very successful in so called collective systems since consist of large numbers of interacting agents that do not necessarily know each other and need to cooperate and interact in a very dynamic and flexible way. A typical example are swarms of robots, where a single robot may need to communicate with every robot “in the same room, within 3 meters of distance, able to push and pull objects, with more than 66% of battery left, …”. The goal of this project is to apply such attribute-based communication to social networks (Facebook, Twitter, and so on) where, typically, the means of communication are limited to very tightly ones: direct messages, mentions, wall posting, etc.