File Refinement

 

Title: File Refinement
Authors: Karen Zee and Viktor Kuncak
Submission date: 2004-12-09
Abstract: These theories illustrates the verification of basic file operations (file creation, file read and file write) in the Isabelle theorem prover. We describe a file at two levels of abstraction: an abstract file represented as a resizable array, and a concrete file represented using data blocks.
BibTeX:
@article{FileRefinement-AFP,
  author  = {Karen Zee and Viktor Kuncak},
  title   = {File Refinement},
  journal = {Archive of Formal Proofs},
  month   = dec,
  year    = 2004,
  note    = {\url{http://isa-afp.org/entries/FileRefinement.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License