Research
We develop rigorous methods, from formal models to testing and security analysis, to build autonomous systems that people can depend on.
Modern systems are increasingly decentralised and autonomous, and therefore increasingly difficult and error-prone to build. Drones, robots, vehicles, industrial plants and microservice platforms must provide continuous service, tolerate faults, adapt to change and resist attacks, and they must do all this while protecting the data and privacy of their users. In embedded and cyber-physical systems, a software misbehaviour can have disruptive effects on the surrounding physical world.
More and more often, the autonomous components of these systems are driven by artificial intelligence: perception based on deep learning, and agents built on large language models (LLMs) that plan, take decisions and act on their own. These technologies are remarkably useful, but they are statistical in nature. They can fail in unexpected ways, be manipulated through adversarial inputs such as prompt injection, and their behaviour is hard to specify and verify. Finding ways to integrate them safely into critical systems is one of the great open challenges of our time, and one we want to help solve.
Dependability is the umbrella term for the qualities all these systems need: availability, reliability, safety, integrity, confidentiality and maintainability. MADS works on the main ways to achieve them, whether a system is built from conventional software or from AI-based agents: preventing faults through correct-by-construction design, removing them through testing and verification, and protecting systems against malicious attacks.
Attributes of dependability
Research areas
Finding failures before users do: automated test generation and quality assurance for complex software, AI-based and self-adaptive systems.
Breaking and fixing real systems: security of protocols, networks and industrial devices, from formal verification to hands-on vulnerability research.
Correct by construction: choreographic languages, types and formal models for coordinating fleets of autonomous, distributed agents.
Foundations
Since its foundation in 2013, the lab has contributed to the theory of distributed and concurrent systems. This background is shared by all our research areas.
Process calculi, bigraphical reactive systems, coalgebraic semantics and behavioural equivalences.
Type theory, categorical semantics and proof assistants for certified reasoning about programs.
Languages and strategies for coordinating distributed, autonomous components, including transactions and choreographies.
Verification of security properties of authentication and communication protocols.
Engineering techniques to implement trustworthy systems on constrained and embedded devices.
Joint projects with companies on testing, vulnerability assessment and secure system design.