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 JanDisplayed time zone: Saskatchewan, Central America change
10:30 - 12:30
|Extending the Profile Abstraction for Complete Entailment Checking of Symbolic Heaps of Bounded Treewidth|
|Steel: scaling up memory reasoning for F*|
|The Lower Bound of Decidable Entailments in Separation Logic with Inductive Definitions|
ADSLPre-print File Attached