The Challenge of Hardware-Software Co-Verification

---

Panagiotis Manolios.
VSTTE, IFIP Working Conference on Verified Software: Theories, Tools, Experiments, Part of ETH's 150th anniversary celebration. Zurich, October 2005. © Springer-Verlag

Abstract

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