F* PoP Up Seminar

Time: Next event on Tuesday, May 2, 2023 (5am Pacific Daylight Time, 10pm Australian Eastern Standard Time)
Speaker: Amos Robinson on Pipit: early work verifying reactive control systems in F*
Location: Zoom
Youtube channel: YouTube
Join fstar-mailing-list@googlegroups.com for future announcements.

Overview


F* is a Proof-oriented Programming Language that allows writing programs and proofs about them within a single framework. Software components developed and proven correct and secure in F* have been deployed in various production systems, including Microsoft Windows Hyper-V, Microsoft Azure, the Linux kernel, and Firefox.

The F* PoP Up Seminar is a monthly event aimed at bringing together the F* community. It is a discussions-oriented, informal seminar where the attendees may:

Each event in the seminar will be at most one-hour long, featuring one or more presenters who will lead the discussion. The sessions will be interactive, may involve code walkthroughs, deep-dive discussions, live coding, detailed proof debugging, and maybe even some slides!

To propose a talk, send an email to the Google group with the following details:

We look forward to your proposals!

Schedule


Date Speaker(s) Topic
May 2, 2023 (5am PDT) 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.

December 6, 2022 (830am PDT) Nik Swamy Understanding how F* uses Z3 (YouTube, Chapter)
October 11, 2022 (830am PDT) Guido Martinez Tactics and Metaprogramming (YouTube, Demo code samples, Draft chapter)
September 6, 2022 (830am PDT) Jay Bosamiya vWasm: Verified Software Sandboxing using F* (related paper, from USENIX Security 2022), YouTube
August 9, 2022 Alex Rozanov Abstract Algebra in F* (Slides, YouTube)
July 12, 2022 (first half) Vimala Soundarapandian Replicated Data Types (YouTube, Code)
July 12, 2022 (second half) Lucas Franceschino A REPL for Tactics in F* (YouTube)

Organizers