Separation logic-based verification atop a binary-compatible filesystem model

DOI10.1007/978-3-030-63882-5_10MaRDI QIDQ2038034zbMATH OpenOpenAlexFDO

Authors Mihir Parang Mehta, William R. Cook

Publication date 8 July 2021

Full work available at URL https://doi.org/10.1007/978-3-030-63882-5_10

zbMATH Keywords

filesystemsseparation logictheorem proving

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Computer Science Logic
• A mini challenge: build a verifiable filesystem
• Connecting higher-order separation logic to a first-order outside world
• VST-Floyd: a separation logic tool to verify correctness of C programs
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic

Cited in

(3)

• An adaptation-complete proof system for local reasoning about cloud storage systems
• Reasoning about block-based cloud storage systems via separation logic
• A mini challenge: build a verifiable filesystem

Describes a project that uses

Uses Software

• ACL2

This page was built for publication: Separation logic-based verification atop a binary-compatible filesystem model

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2038034)