Pancake is a research programming language for systems programming developed at Chalmers University of Technology, ANU, and UNSW. It is implemented in the theorem prover HOL4 and comes with a formally verified compiler and is built from the ground up for predictable compilation and ease of verification.
We have a prototype transpiler that translates annotated Pancake programs into Viper, which we then feed to SMT-backends for verification. We have used this framework to verify an Ethernet driver. In order to improve the guarantee that the framework provides, we plan to verify the correctness of the transpiler itself.
The project is to refactor and reimplement this transpiler to make it more amenable to verification. Specifically, we aim to reimplement it either in CakeML or directly in the theorem prover HOL4 (it is currently implemented in Rust), to improve its parsing phase, and to remove dependency on an external tool.
School
Computer Science and Engineering
Research Area
Formal methods | Formal verification | Programming language | Operating systems
Suitable for recognition of Work Integrated Learning (industrial training)?
Yes
- 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.
- Report outlining the approach taken, tradeoffs considered and work done.
- Pull request to the Trustworthy Systems Group's github repository with implementations.
