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
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

adsl-2020-papers
10:30 - 12:30: ADSL 2020 - Research Papers at Conde
adsl-2020-papers10:30 - 11:00
Research paper
File Attached
adsl-2020-papers11:00 - 11:30
Research paper
Denis MerigouxINRIA, Aymeric FromherzCarnegie Mellon University
File Attached
adsl-2020-papers11:30 - 12:00
Research paper
File Attached
adsl-2020-papers12:00 - 12:30
Research paper
Mnacho Echenim, Radu IosifVERIMAG, CNRS, Université Grenoble-Alpes, Nicolas Peltier
Pre-print File Attached