manolios@cc.gatech.edu
College of Computing
Building verified computing systems such as a verified compiler
or operating system will require both software and hardware
verification. How can we decompose such verification efforts
into mostly separate tasks, one involving hardware and the other
software? What theorems should we prove? What specification
languages should we use? What tools should we build? To what
extent can the process be automated? We address these issues,
using as a running example our recent and on-going work on
refinement-based pipelined machine verification.
PDF (76K) © Springer-Verlag
|
Last modified: Mon Oct 24 22:06:59 EDT 2005
manolios@cc.gatech.edu |
College of Computing |