- Combining Mechanized Proofs and Model-Based Testing in
the Formal Analysis of a Hypervisor, veröffentlicht in den
Proceedings von FM2016 in LNCS 9995, Seiten 69-84.
Zusammen mit dem FireEye Team Formale Methoden (Hanno, Juan, Ulrich,
Yoichi, Cesar, Keiko,
Jorge und Thomas)
und Jacek.
Kopie: [pdf]
- Formalizing Cut Elimination of Coalgebraic Logics in Coq,
veröffentlicht bei der 22. Conference für Automated Reasoning with Analytic Tableaux and Related
Methods 2013,
LNAI
Band 8123,
Seiten 257-272.
Kopie:
[pdf]
Etwas Dokumentation und die Coq Quellen der Formalisierung sind
auf dieser Seiter
verfügbar (in english only).
- A Probabilistic Quantitative Analysis of
Probabilistic-Write/Copy-Select,
veröffentlicht in den
Proceedings des Nasa Formal Methods Symposiums 2013, LNCS
Band 7871, Seiten 307-321.
Zusammen mit
Christel,
Benjamin,
Sascha,
Steffen and
Marcus Völp.
Kopie: [pdf]
- Chiefly Symmetric: Results on the Scalability of
Probabilistic Model Checking for Operating-System Code,
veröffentlicht im Band 102 der
Electronic Proceedings in Theoretical Computer Science (EPTCS),
Seiten 156-166.
Zusammen mit
Christel,
Marcus Daum,
Benjamin,
Hermann,
Joachim,
Sascha,
Steffen und
Marcus Völp.
Kopie: [pdf]
- On the Use of Underspecified Data-Type Semantics for
Type Safety in Low-Level Code, veröffentlicht in Band 102 der
Electronic Proceedings in Theoretical Computer Science (EPTCS),
Seiten 73-87.
Zusammen mit
Tjark and
Marcus.
Kopie: [pdf]
- Waiting for Locks: How Long Does It Usually Take?,
veröffentlicht im LNCS Band 7437,
Seiten 47-62.
Zusammen mit
Christel,
Marcus Daum,
Benjamin,
Hermann,
Joachim,
Sascha,
Steffen und
Marcus Völp.
Kopie: [pdf]
- Proceedings of the 6th
International Workshop on Systems Software Verification
(SSV 2011), veröffentlicht als
Band 24 of OpenAccess Series in Informatics (OASICS)
von Schloss Dagstuhl.
Zusammen mit Jörg und Marco
(Editoren).
link: [online proceedings]
Ich habe den Tagungsband vorher auch als Technischen Bericht
der TU Dresden, Nummer TUD-FI11-02-August 2011 herausgebracht.
Kopie: [pdf]
- Performance issues of Selective Disclosure and Blinded Issuing
Protocols on Java Card, veröffentlicht in den Proceedings
des Workshops für "Information Security, Theory and Practices" (WISTP 2009), LNCS Band
5746, Seiten 95-111.
Zusammen mit Bart
Jacobs.
Kopien:
[ps.gz]
[pdf]
- Preemption Abstraction: A Lightweight Approach to
Modelling Concurrency, veröffentlicht in den
Proceedings des 14.
Internationalen Workshops für formale Methoden für
kritische Systeme in der Industrie (FMICS 2009),
LNCS 5825, Seiten 149-164.
Zusammen mit
Erik,
Alejandro,
Marko und
Sjaak.
Kopie:
[pdf]
- Formal Memory Models for the Verification of Low-Level
Operating-System Code, veröffentlicht im Journal
of Automated Reasoning, Band 42, Nummer 2-4.
Zusammen mit
Tjark und
Marcus.
Kopie:
[ps.gz]
(Außer der Formatierung und den Seitenzahlen ist die Version
hier identisch mit der im gedruckten Journal)
- Nova interface specification, Robin deliverable
D12, auch als Technischer Bericht ICIS-R08011 des ICIS department
veröffentlicht.
Zusammen mit
Tjark,
Erik,
Marko und
Peter. Siehe auch
meine Seite zum Robin-Projekt.
Kopie:
[ps.gz]
- Nova micro-hypervisor verification, Robin deliverable
D13, mit kleinen Änderungen auch als technischer Bericht
ICIS-R08012 des ICIS department veröffentlicht.
Zusammen mit
Tjark,
Marcus,
Erik,
Marko und
Peter. Siehe auch
meine Seite zum Robin-Projekt.
Kopie des technischen Berichtes:
[ps.gz]
(die Originalversion ist auf der Robin Seite)
- A Formal Model of Memory Peculiarities
for the Verification of
Low-Level Operating-System Code, veröffentlicht in den
Proceedings des 3. Internationalen Workshops zur
Verifikations von Systemsoftware (SSV08), Sydney, ENTCS Band 217,
Seiten 79-96.
Zusammen mit
Tjark und
Marcus.
Kopie
[ps.gz]
- Formal Methods in the Robin project:
Specification and verification of the Nova
microhypervisor, veröffentlicht in den Proceedings des C/C++
Verifikationsworkshops.
Kopie:
[a4 ps.gz]
- Olmar: manipulating C and C++ abstract syntax trees in
Ocaml, veröffentlicht in den Proceedings des C/C++
Verifikationsworkshops.
Kopie:
[a4 ps.gz]
- Micro hypervisor verification:
possible approaches and relevant properties, veröffentlicht in
den Proceedings der "NLUUG Voorjaarsconferentie" 2007.
Kopie:
[a4 ps.gz]
- Specification and verification of the Nova
microhypervisor, Robin D.6 deliverable. Zusammen mit Bart Jacobs, Erik
Poll, Marko van Eekelen und Peter van Rossum.
Kopien:
[Gekürzte Version ps.gz]
[Vollständige Version ps.gz]
- The VFiasco approach for a verified operating
system,
Zusammen mit Michael,
veröffentlicht in den Proceedings des 2. ECOOP
Workshops für Programmiersprachen und Betriebssysteme.
Kopie:
[a4 ps.gz]
- Verifying Duff's device: A simple compositional
denotational semantics for Goto and computed jumps,
unveröffentlicht.
Kopie:
[ps.gz]
- Predicate and Relation Lifting for Parametric
Algebraic Specifications,
Proceedings von CMCS 04, ENTCS Band 106, Seiten 335-353.
Kopie:
[a4 ps.gz]
- The Semantics of C++ Data Types: Towards Verifying
low-level System components, Zusammen mit Michael.
Veröffentlicht in den "Emerging Trends Proceedings" von
TPHOLs 2003 im
Technischen
Bericht No. 187 des Instituts für Informatik
Universität Freiburg.
Kopie:
[a4 ps.gz]
- Coalgebraic Methods for Object-Oriented
Specification,
Doktorarbeit, TU Dresden. Siehe diese Seite.
- The Coalgebraic Class Specification Language CCSL
-Syntax and Semantics-,
TU Dresden Technischer Bericht TUD-FI02-08-August 2002.
Kopien
[a4 2up ps.gz]
[a4 ps.gz]
- Applying source-code verification to a
microkernel,
Zusammen mit Michael
Hohmuth und Shane G.
Stephens.
TU Dresden Technischer Bericht TUD-FI02-03-März 2002.
Kopie
[a4.ps.gz]
Eine 5-seitige Kurzfassung wurde in den Proceedings des 10.
"ACM SIGOPS European Workshop", 2002 veröffentlicht.
Kopie
[a4-abstr.ps.gz]
- Greatest Bisimulations for Binary Methods,
veröffentlicht in ENTCS Volume 65 (CMCS '02).
Das ist quasi eine Vortsetzung meines Artikels
"Coalgebras for Binary
Methods ..." in dem zwei neue Resultate für
Vereinigungen von Bisimulationen beschrieben werden.
Das online Material (Formalisierung in PVS) ist
hier verfügbar.
Kopie
[a4.ps.gz]
- Assertional and Behavioural Refinement in Coalgebraic
Specification Zusammen mit
Bart Jacobs.
Das ist der Artikel zu einem eingeladenen Vortrag von Bart.
Leider haben es die Organisatoren dieses Workshops oder der
Konferenz nicht geschafft Proceedings herauszugeben...
Abschnitt 6 enthält eine kleine Fallstudie zu einem
Transaktionsmechanismus in CCSL. Siehe hier.
Kopie
[a4.ps.gz]
- Coalgebras for Binary
Methods: Properties of Bisimulations and Invariants
im Journal
"Theoretical
Informatics and Applications" 35(1):83-111.
(Das ist eine stark erweiterte Version meines Artikels
Coalgebras for Binary Methods von CMCS '00)
Das online Material (Formalisierung in PVS) is
here verfügbar.
Kopie [a4.ps.gz]
- VFiasco - Towards a Provably Correct Microkernel,
Technical Bericht TUD-FI01-1
Zusammen mit Hermann Härtig
und
Michael
Hohmuth.
Kopie [a4.ps.gz]
- The Coalgebraic Class Specification
Language CCSL Zusammen mit Jan Rothe und
Bart Jacobs.
"Journal of Universal
Computer Science" 7(2):175-193.
Kopien [full-paper.ps.gz]
[extended-abstract.ps.gz]
- Case study in
coalgebraic specification: Memory management in the Fiasco
microkernel. Technischer Bericht TPG2/1/2000 des SFB 358.
Die Fallstudie selbst, ist mit allen Quellen
online verfügbar.
Kopie [paper.ps.gz]
- Coalgebras for Binary Methods,
veröffentlicht in ENTCS Band 33 (CMCS '00).
(Eine stark erweiterte Version ist unter dem Titel
Coalgebras for Binary Methods: Properties of
Bisimulations and Invariants verfügbar.)
Das online Material (Formalisierung in PVS)
ist hier verfügbar.
Kopie [paper-a4.ps.gz]
- Reasoning about Java Classes,
Zusammen mit Marieke,
Bart,
Joachim, Martijn und
Uli
veröffentlicht in den Proceedings von OOPSLA '98.
Kopie [a4.ps.gz]
- Reasoning about Classes in Object-Oriented
Languages: Logical Models and Tools,
Zusammen mit Marieke,
Uli und
Bart
(veröffentlicht in den Proceedings von ESOP '98)
Kopie [a4.ps.gz]
- Mein Diplom [Kopie a4.ps.gz]
- Mein großer Beleg [Kopie a4.ps.gz]