A mini challenge: build a verifiable filesystem

DOI10.1007/S00165-006-0022-3MaRDI QIDQ2643130zbMATH OpenOpenAlexFDO

Authors Rajeev Joshi, Gerard J. Holzmann

Publication date 23 August 2007

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00165-006-0022-3

zbMATH Keywords

Filesystem designFormal verificationVerification grand challenge

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Recommendations

• POSIX file store in Z/Eves: An experiment in the verified software repository
• Separation logic-based verification atop a binary-compatible filesystem model
• scientific article; zbMATH DE number 1956470
• Mechanising a formal model of flash memory
• Verification, Model Checking, and Abstract Interpretation

Cites work

• scientific article; zbMATH DE number 1956470 (Why is no real title available?)
• Specification of the UNIX Filing System

Cited in

(12)

• Mechanising a formal model of flash memory
• POSIX file store in Z/Eves: An experiment in the verified software repository
• Proving the correctness of client/server software
• Separation logic-based verification atop a binary-compatible filesystem model
• Formalizing a hierarchical file system
• New Challenges in Model Checking
• Generating Tests from B Specifications and Test Purposes
• Formalizing a hierarchical file system
• scientific article; zbMATH DE number 1956470 (Why is no real title available?)
• Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning
• Extended Static Checking by Calculation Using the Pointfree Transform
• Generating tests from B specifications and dynamic selection criteria

This page was built for publication: A mini challenge: build a verifiable filesystem

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