Programming languages

The design, specification and implementation of programming languages is essential for building trustworthy systems. Programs expressed in well-designed languages are easier to specify, verify, optimise, and maintain.

Pancake

Pancake is a new low-level programming language designed specifically for the verification of device drivers and other low-level system programs. Pancake compiler reuses significant parts of the CakeML compiler backend, which is formally verified.

CakeML

CakeML is a verified compiler for a high-level functional language, suitable for application-level software.

CakeML is a collaborative project by researchers at multiple institutions. Here at Trustworthy Systems, our work focuses on applying CakeML to systems programming, and verifying the behaviour of CakeML programs in the context of larger systems.

L4.verified C semantics

We have developed a detailed formalisation of a large subset of the C language. This is implemented in our C parser and is used for our verification of seL4.