sysma logo
Research in computer science, carried out within the SysMA unit, deals with the development of languages and techniques for the analysis and verification of concurrent and distributed systems.

Our goal is to push the use of formal methods as methodological and automatic tools for the development of high-quality, correct software and systems that are fast, usable, re-usable, maintainable, and modular.

To make our tools usable by programmers not acquainted with the underlying mathematical foundations; we aim at effective but disappearing formal methods.

Our main areas of expertise are concurrency theory, programming languages, and software engineering, with a wide range of applications such as adaptive systems, cyber-physical systems, cloud computing, computational biology, fault-tolerant systems, security and transportation networks. Specific topics include:

Foundations of concurrent systems

  • Process algebras
  • Behavioural equivalences
  • Reversible computing

Programming Languages

  • Languages for network aware programming
  • Languages for service-oriented programming
  • Languages for autonomic and adaptive programming

Quantitative Analysis

  • Markov chains
  • Differential equations
  • Simplification and abstraction techniques

Software Engineering

  • Self-adaptive systems
  • Software performance
  • Software product lines

Systems Verification

  • Temporal logics
  • Model checking
  • Type systems