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

DOI10.1007/978-3-030-63882-5_10zbMath1475.68094OpenAlexW3109504427MaRDI QIDQ2038034

William R. Cook, Mihir Parang Mehta

Publication date: 8 July 2021

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

zbMATH Keywords

theorem provingseparation logicfilesystems

Mathematics Subject Classification ID

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

Uses Software

• ACL2

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