Mechanising a formal model of flash memory

DOI10.1016/J.SCICO.2008.09.014MaRDI QIDQ1004295zbMATH OpenOpenAlexFDO

Authors Andrew Butterfield, Leo Freitas, Jim 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.09.014

zbMATH Keywords

verificationtheorem provingflash hardwaregrand challenge

Mathematics Subject Classification ID

Computer system organization (68M99)

Recommendations

• Flash memory efficient LTL model checking
• Formal memory models for the verification of low-level operating-system code
• A Unified Memory Model for Pointers
• POSIX file store in Z/Eves: An experiment in the verified software repository
• A mini challenge: build a verifiable filesystem

Cites work

• scientific article; zbMATH DE number 42431 (Why is no real title available?)
• scientific article; zbMATH DE number 1956470 (Why is no real title available?)
• A mini challenge: build a verifiable filesystem
• Specification of the UNIX Filing System
• Z/Eves and the Mondex Electronic Purse

Cited in

(3)

• Formalizing a hierarchical file system
• Flash memory efficient LTL model checking
• A mini challenge: build a verifiable filesystem

Describes a project that uses

Uses Software

• Z
• Z/EVES

This page was built for publication: Mechanising a formal model of flash memory

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