F* PoP Up Seminar: Pipit, early work verifying reactive control systems in F*

[Nikhil Swamy]

We're resuming the PoP Up Seminar series after a break of a few months. But, this one should be really fun. Thanks Amos!

Speaker: Amos Robinson

Pipit: early work verifying reactive control systems in F*

Safety-critical control systems, such as the anti-lock braking systems in most cars today, need to be correct and execute in real-time. We could write these systems directly in an imperative language such as LowStar and verify them, but it can be difficult to state high-level specifications about such low-level implementations. Another approach, favoured by large parts of the aerospace industry, is to implement the controllers in a high-level language such as Lustre or SCADE, and verify that the implementations satisfy the high-level specification using a model-checker. These model-checkers can prove many interesting properties automatically, but do not provide many options when the automated proof techniques fail.

In this talk I will describe my preliminary work on Pipit, an embedded domain-specific language for implementing and verifying such controllers in F*. Pipit aims to provide a high-level language similar to Lustre, while reusing F*'s proof automation and manual proofs for verifying controllers, and using LowStar's C-code generation for real-time execution. Pipit translates its expression language to a transition system for k-inductive proofs, which is mostly verified; verifying the translation to imperative code is future work.

---

Amos Robinson did his PhD in streaming programming languages and stream fusion at UNSW in Sydney, Australia. For the past three years he was working at a self-driving car company where he verified these sorts of control systems. He has just started a postdoc at the Australian National University, where he will be working with Alex Potanin. (edited)