Pancake is a research programming language for systems programming under development at Chalmers University of Technology, ANU, and UNSW. It comes with a formally verified compiler and is built from the ground up for predictable compilation and ease of verification.
We have a transpilation tool ("transpiler") that converts annotated Pancake code into Viper, an intermediate language for an SMT-backend. These annotations encode the pre- and post-conditions that specify the behaviour of the Pancake code in a pseudo-Viper syntax. We then verify that the code correctly implements the specification by sending the transpiled Viper files to the SMT-backend.
The aim of this project is to explore the ways to represent these annotations directly in HOL4 interactive theorem prover, most likely as a Hoare logic. This work can leverage the currently on-going work on Viper semantics in HOL4, which is likely to provide a basis for semantics for annotated Pancake.
School
Computer Science and Engineering
Research Area
Formal methods | Program logic | Program semantics
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.
