Mechanising a formal model of flash memory

DOI10.1016/j.scico.2008.09.014zbMath1162.68387OpenAlexW2039336509MaRDI QIDQ1004295

Andrew Butterfield, 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.09.014

zbMATH Keywords

verificationtheorem provingflash hardwaregrand challenge

Mathematics Subject Classification ID

Computer system organization (68M99)

Related Items (2)

Flash memory efficient LTL model checking ⋮ Formalizing a hierarchical file system

Uses Software

• Z/EVES
• Z

Cites Work

• Unnamed Item
• Unnamed Item
• A mini challenge: build a verifiable filesystem
• Specification of the UNIX Filing System
• Z/Eves and the Mondex Electronic Purse

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