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

Опубликовано 3 сентября 2019, 21:47

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.

See more at microsoft.com/en-us/research/v...