POSIX file store in Z/Eves: An experiment in the verified software repository

DOI10.1016/J.SCICO.2008.08.001zbMath1162.68388OpenAlexW1982220991MaRDI QIDQ1004296

Zheng Fu, Leo Freitas, J. C. P. Woodcock

Publication date: 2 March 2009

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.scico.2008.08.001

zbMATH Keywords

verificationtheorem provingfile systemsflash memorygrand challengePOSIX

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Computer system organization (68M99)

Related Items (3)

Formalizing a hierarchical file system ⋮ Formalizing a Hierarchical File System ⋮ POSIX file store in Z/Eves: An experiment in the verified software repository

Uses Software

• JML
• Z/EVES
• Z

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• POSIX file store in Z/Eves: An experiment in the verified software repository
• A mini challenge: build a verifiable filesystem
• Specification of the UNIX Filing System
• Z/Eves and the Mondex Electronic Purse
• Proving Theorems About JML Classes
• Proofs and Refutations

This page was built for publication: POSIX file store in Z/Eves: An experiment in the verified software repository