Steel: A Concurrent Separation Logic Framework to Scale Up Verification in F*

  • Aymeric Fromherz, Denis Merigoux | Carnegie Mellon University, Inria

In recent years, the F* ecosystem has been successfully used to formally verify real-world applications ranging from parsers to cryptographic providers. Nevertheless, verification  is still time-consuming, and scaling up is still challenging due to (1) lack of modularity when reasoning about the heap, (2) explosion of state-related SMT context and (3) model limited to sequential programming.

In this talk, we present Steel, a concurrent separation logic abstraction on top of the existing F* framework. Steel offers a modular resource-based memory model with permissions, using a mix of SMT solving and F* tactics to discharge its proof obligations. Steel also enables the specification and verification of concurrent programs in a fork-join concurrency model.

[Slides]

Watch Next