Mu: A Micro-Virtual-Machine for Managed Languages
Mu is a micro-virtual-machine targeted at managed languages and intended as a verification target.
A formally verified, optimising ML compiler, developed in collaboration with Cambridge, Chalmers, and Kent.
Concurrency and Protocol Verification
Formal models of concurrency and distributed systems for the specification, analysis and verification of network protocols and operating systems.
Mixed-Criticality Real-Time Systems
Microkernel mechanisms and execution time models for building complex systems that not only deliver, but deliver on time.
The Trustworthy Systems project is the overarching project of the Trustworthy Systems Research Group. Its aim is to fundamentally change […]
High Assurance Cyber Military Systems
Using formal proof and microkernel mechanisms to build secure autonomous vehicles in DARPA’s high assurance cyber military systems (HACMS) program.
seL4 is a high-assurance, high-performance microkernel developed and formally verified by the Trustworthy Systems Group at Data61. It is the world’s most […]