Open AccessVerified Safety and Information Flow of a Block Device
Author(s) -
Paul Graunke
Publication year - 2008
Publication title -
electronic notes in theoretical computer science
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.242
H-Index - 60
ISSN - 1571-0661
DOI - 10.1016/j.entcs.2008.06.049
Subject(s) - rewriting , computer science , information flow , adaptation (eye) , programming language , block (permutation group theory) , work flow , work (physics) , software engineering , flow (mathematics) , software , theoretical computer science , industrial engineering , mathematics , engineering , linguistics , mechanical engineering , philosophy , physics , geometry , optics
This work reports on the author's experience designing, implementing, and formally verifying a low-level piece of system software. The timing model and the adaptation of an existing information flow policy to a monadic framework are reasonably novel. Interactive compilation through equational rewriting worked well in practice. Finally, the project uncovered some potential areas for improving interactive theorem provers
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom