Publikationen

• 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]

Startseite Wissenschaft Überblick Alle Publikationen Vorträge Doktorarbeit CCSL Robin