| V | E | R | I | F | I | E | D |
 |
 |
 |
 |
 |
 |
- Overview
- Papers and reports
- VFiasco FAQ
- Subprojects
- Download!
- Student jobs - We're hiring!
- Related work
- Project website (Internal access only)
- Lecture *
Quick links:
Papers and reports
- |
Michael Hohmuth, Hendrik Tews: The VFiasco approach for a verified operating system. Accepted at the 2nd ECOOP Workshop on Programm Languages and Operating Systems (ECOOP-PLOS'05) | |
- |
Endrawaty: Verification of the Fiasco IPC Implementation. Master Thesis 2004 | |
- |
Hendrik Tews: Verifying Duff's device: A simple compositional denotational semantics for Goto and computed jumps. | |
- |
Michael Hohmuth, Hendrik Tews: The Semantics of C++ Data Types: Towards Verifying low-level Systems Code. (Emerging trends track on TPHOLs 2003, 2003) | |
- |
Michael Hohmuth, Hendrik Tews, Shane G. Stephens: Applying source-code verification to a microkernel - The VFiasco project. (TU Dresden Technical Report, 2002) | |
|
Extended Abstract of this
paper [updated] (This extended abstract appears in the proceedings of the 10th ACM SIGOPS European Workshop, 2002) | ||
- |
Matthias Daum: Development of a semantics compiler for C++ (Diploma thesis, 2003) | |
- |
Sarah Hoffmann: Formalising PC Hardware: A Model of the x86 Architecture (Diploma thesis, 2003) | |
- |
Matthias Daum: Entwicklung einer Implementationssprache für einen sicheren Mikrokern (TU Dresden term paper, 2002; in German only) | |
- |
Hendrik Tews, Hermann Härtig, Michael Hohmuth: VFiasco - Towards a Provably Correct Microkernel (TU Dresden Technical Report, 2001) | |
- |
Michael Hohmuth, Hendrik Tews: Work-in-Progress Report: VFiasco - Towards a Provably Correct Microkernel (Presented at USENIX Annual Technical Conference 2001) | |
- |
Horst Reichel, Hermann Härtig: Antrag auf eine DFG-Sachbeihilfe Application for funding the VFiasco project (in German only). Contains the (preliminary) working schedule. (2001) | |
- |
Hendrik Tews: Case study in coalgebraic specification: Memory management in the Fiasco microkernel (TU Dresden Technical Report, 2000) | |
- |
Michael Hohmuth: The Fiasco Kernel: Requirements Definition (TU Dresden Technical Report, 1998) | |
- |
Michael Hohmuth: The Fiasco Kernel: System Architecture (Unpublished manuscript) |
|
- |
Jochen Liedtke: L4 Reference Manual (GMD/ IBM Watson Technical Report, 1996) |
View other publications from TU Dresden's Operating Systems group
11 Jul 2005