Computer Science and Engineering
Pancake is a new programming language aimed at enabling the verification of device drivers. The language itself is still under development. This project is to evaluate the current Pancake language by using it to implement drivers of various complexity and providing feedback to the language developers.
School
Research Area
Operating systems | Programming languages
- Research Environment
- Expected Outcomes
- Supervisory team
- Reference Material/Links
The Trustworthy Systems (TS) Group is the pioneer in formal (mathematical) correctness and security proofs of computer systems software. Its formally verified seL4 microkernel, now backed by the seL4 Foundation, is deployed in real-world systems ranging from defence systems via medical devices, autonomous cars to critical infrastructure. The group's vision is to make verified software the standard for security- and safety-critical systems. Core to this a focus on performance as well as making software verification more scalable and less expensive.
- Sample device drivers written in Pancake, ranging from simple serial drivers to drivers for more complex devices, a stretch goal would be an Ethernet driver.
- Report outlining the experience with Pancake, discussion of limitations and other shortcomings, and suggestions for improvement.
