Pancake is a research programming language currently under development at UNSW, Chalmers University, ANU, and Gothenburg University. It comes with a compiler that is verified correct using the HOL4 theorem prover, and is built from the ground up for predictable compilation and ease of verification.
We have verified some properties of an ethernet driver written in Pancake by annotating the code with necessary conditions and translating it into Viper, an intermediate language, and then feeding it to SMT backends.
The aim of this project is to produce more test cases (i.e., drivers written in Pancake with annotations) for this Pancake-to-Viper verification framework and then to compare and evaluate them, with an aim to assess its efficiency and provide data points for further improvements.
School
Computer Science and Engineering
Research Area
Formal methods | Programming languages | Formal verification
- 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.
