| Home |
| About |
| Submission Guidelines |
| Search |
| Download |
project summary
File Refinement
| Title: | File Refinement |
| Author: | Karen Zee and Viktor Kuncak |
| Submisison 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. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
Older releases:
|