Real-time systems, such as the microcontroller that controls the brakes in a modern car, have strict bounds on the memory usage and compute time: a delay could be disastrous. For systems implemented in low-level languages such as C, it can be difficult to ensure that the compute time is always bounded, or that memory will never leak. One approach, used in the aerospace industry, is to write these real-time systems in a reactive language, which is a restricted language that gives strong guarantees on the runtime bounds. In addition to providing these guarantees on execution requirements, reactive languages often also provide ways to verify that the programs do the right thing.
Pipit is a small reactive language for implementing and verifying such real-time systems. It is implemented and partially verified in the F* theorem prover, and it generates real-time C code for execution on microcontrollers. Pipit is very restricted at the moment and only provides core operations. It currently lacks a foreign-function interface (FFI), which is required to call external imperative code. As Pipit is a (partially) verified compiler, adding an FFI would require a mixture of formalising the semantics of foreign functions as well as compiler engineering and, depending on your interest, proof engineering.
Requirements
The size of this project can be adapted to suit students of any level, and the exact project can be adjusted to suit your interests. It will involve formally reasoning about the semantics of programs, so a course such as COMP3610 (Principles of Programming Languages) or familiarity with Hoare logic (covered in COMP1600) would be ideal, as well as familiarity with a functional language such as Haskell or ML.