F* PoP Up Seminar

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.