Formal verification of effectful programs in F*
Organization
Laboratory for Software Science
Abstract
Formal verification of effectful programs in F*
F* [1] is a general-purpose proof-oriented programming language, supporting both purely functional and effectful programming. It combines the expressive power of dependent types with proof automation based on SMT solving and tactic-based interactive theorem proving. It has an excellent support for reasoning about programs containing computational effects (state, exceptions, IO, nondeterminism, etc) based on Dijkstra monads [2] and layered indexed effects [3], and then extracting such verified code to runnable OCaml, C, and Rust.
A thesis in this area would involve learning F* and using its effect system to specify and verify the correctness of some effectful programs or algorithms. One of the goals of the thesis would be to demonstrate that F* is a good tool for a hybrid style of program verification: you can focus on formally verifying certain critical aspects of a piece of software, while postulating in an abstract interface that the rest of the software behaves as intended by the programmer.
For example, one example project idea in this area is to use the Steel and Pulse frameworks [4] of F* to verify the correctness of some embedded IoT software, written in C or Rust, and running on small microcontrollers, such as on ESP32. For a better idea of the work involved, [5] demonstrates the use of the older Low* framework in F* for specifying and verifying the memory-safety of simple ESP32 programs installing interrupt handlers and reacting to interrupts.
Any potential students are of course very welcome to propose their own ideas about which effectful programs or algorithms to specify and verify in F*. Students interested in the verification of algorithms in other dependently typed programming languages (e.g., Agda) are also welcome to get in contact.
[1] https://fstar-lang.org
[2] https://arxiv.org/abs/1903.01237
[3] https://www.fstar-lang.org/papers/indexedeffects/indexedeffects.pdf
[4] https://fstar-lang.org/tutorial/book/pulse/pulse.html
[5] https://github.com/danelahman/esp32-fstar
F* [1] is a general-purpose proof-oriented programming language, supporting both purely functional and effectful programming. It combines the expressive power of dependent types with proof automation based on SMT solving and tactic-based interactive theorem proving. It has an excellent support for reasoning about programs containing computational effects (state, exceptions, IO, nondeterminism, etc) based on Dijkstra monads [2] and layered indexed effects [3], and then extracting such verified code to runnable OCaml, C, and Rust.
A thesis in this area would involve learning F* and using its effect system to specify and verify the correctness of some effectful programs or algorithms. One of the goals of the thesis would be to demonstrate that F* is a good tool for a hybrid style of program verification: you can focus on formally verifying certain critical aspects of a piece of software, while postulating in an abstract interface that the rest of the software behaves as intended by the programmer.
For example, one example project idea in this area is to use the Steel and Pulse frameworks [4] of F* to verify the correctness of some embedded IoT software, written in C or Rust, and running on small microcontrollers, such as on ESP32. For a better idea of the work involved, [5] demonstrates the use of the older Low* framework in F* for specifying and verifying the memory-safety of simple ESP32 programs installing interrupt handlers and reacting to interrupts.
Any potential students are of course very welcome to propose their own ideas about which effectful programs or algorithms to specify and verify in F*. Students interested in the verification of algorithms in other dependently typed programming languages (e.g., Agda) are also welcome to get in contact.
[1] https://fstar-lang.org
[2] https://arxiv.org/abs/1903.01237
[3] https://www.fstar-lang.org/papers/indexedeffects/indexedeffects.pdf
[4] https://fstar-lang.org/tutorial/book/pulse/pulse.html
[5] https://github.com/danelahman/esp32-fstar
Graduation Theses defence year
2024-2025
Supervisor
Danel Ahman
Spoken language (s)
Estonian, English
Requirements for candidates
Level
Bachelor, Masters
Keywords
Application of contact
Name
Danel Ahman
Phone
E-mail