1 - 3 September | Vancouver, Canada BC View More Details & Registration The schedule is subject to change, so please check back before the event for the most up-to-date information.
Please note that all session times are listed below in Pacific Daylight Time (PDT), UTC-7.
Sign up or log in to add sessions to your schedule and sync them to your phone or calendar.
Pancake is a verification-friendly, imperative low-level language for systems programming, which the Trustworthy Systems group at UNSW has been working on to produce verified LionsOS components. Since first introduced in 2024 seL4 Summit, TS continued with Pancake development and Pancake is now mature enough for our systems engineers to take up and port various components originally written in C to Pancake.
In this talk, we report on various recent updates on Pancake and its roadmap, in the broader context of LionsOS. We’ll cover the progress and plans for the general Pancake language extensions and compiler improvements as well as verification of programs written in Pancake, in particular device drivers, both via interactive theorem proving and SMT-based tools.
We’ll highlight the SMT-based approach via Pancake-to-Viper transpiler as a way towards TS’s vision of making verified software the standard for security- and safety-critical systems, aiming to make software verification more scalable and less expensive.
