Interests

  • 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.

Teaching

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

Papers

  • Many-to-many Information Flow Policies (COORDINATION 2017) []
  • Asynchronous Distributed Execution Of Fixpoint-Based Computational Fields (LMCS 2017) [pdf]
  • A coordination language for databases (LMCS 2017) [pdf]
  • Statistical Model Checking for Product Lines (ISOLA 2016) [pdf]
  • Microservices: yesterday, today, and tomorrow (PAUSE 2017)  [draft]
  • Discretionary Information Flow Control for Interaction-Oriented Specifications (Festschrift Meseguer) [pdf ]
  • Replicating Data for Better Performances in X10 (Festschrift Nielson & Nielson) [pdf ]
  • Statistical Analysis of Probabilistic SPL Models with Quantitative Constraints (SPLC 2015) [pdf ]
  • AVOCLOUDY: A Simulator of Volunteer Clouds (SPE) [ pdf]
  • Replica-based High-Performance Tuple Space Computing (COORDINATION 2015) [ pdf]
  • Klaim-DB: A Kernel Language for Distributed Databases (COORDINATION 2015) [pdf]
  • A Fixpoint-based Calculus for Graph-shaped Computational Fields (COORDINATION 2015) [ pdf]
  • The SCEL Language (Software Engineering for Collective Autonomic Systems) [ pdf]
  • Perspectives on Adaptation (Software Engineering for Collective Autonomic Systems) [ pdf]
  • A White Box Perspective on Behavioural Adaptation (Software, Services, and Systems) [pdf]
  • Constraint Design Rewriting (Science of Computer Programming) [ ]
  • Can we efficiently verify concurrent programs under RMMs in Maude? (WRLA 2014) []
  • Programming and Verifying Component Ensembles (From Programs to Systems) []
  • Reputation-based Cooperation in the Clouds (IFIP TM 2014) []
  • A Computational Field Framework for Collaborative Volunteer Clouds (SEAMS 2014) []
  • Modelling and analyzing self-assembling strategies (Science of Computer Programming) [ ]
  • full list or check , , scopus, orcid, isi

Talks

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

Projects

  • 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
  • : European FP6 Project on Software Engineering for Service-Oriented Computing

Conferences and Journals

Alumni

  • Marina Andric (PhD student @ IMT Lucca, Italy)
  •  (Researcher @ Xerox Research Centre, India)
  • Andrea Vandin (Assistant Professor @ IMT Lucca, Italy)

Software Tools

  • pSpaces: Programming with Spaces
  • HSF-SPIN: an extension of the Spin model checker with directed model checking algorithms
  • Promela Database: a collection of Promela models for the Spin model checker

Student Projects

  • BSc/MSc projects: contact  or see some project proposals here or here.
  • PhD projects: scholarships from DTU Compute are advertised here.
  • Industry BSc/MSc/PhD projects: see .