Write a Blog >>
Mon 20 Jan 2020 11:00 - 11:30 at Conde - Research Papers

We present Steel, a semi-automated separation logic framework for the F* proof assistant. Steel is built as a set of verified libraries on top of an existing C-like subset language and memory model, Low*. It relies on the careful mixing of separation logic terms describing the heap together with functional specifications to offer an improved proof development experience compared to current Low*, already used for large-scale projects going over several thousands lines of code. While manipulation of separation logic terms is ensured by F* tactics, the rest of the functional verification conditions is still discharged to the Z3 theorem prover. Bundling fractional permissions and a basic fork-join concurrency model, Steel is designed to automate by tactics the most common patterns of separation logic proofs such as the application of the frame rule in a populated context. While lacking proper evaluation and currently suffering from F* tactics performance issue, we hope to demonstrate its usefulness in the coming year.

Steel: scaling up memory reasoning for F* (presentation.pdf)554KiB

Mon 20 Jan

Displayed time zone: Saskatchewan, Central America change