Publications

• Chiefly Symmetric: Results on the Scalability of Probabilistic Model Checking for Operating-System Code, published in volume 102 in Electronic Proceedings in Theoretical Computer Science (EPTCS), pages 156-166. Done together with Christel, Marcus Daum, Benjamin, Hermann, Joachim, Sascha, Steffen and Marcus Völp.
  copy: [pdf]

• On the Use of Underspecified Data-Type Semantics for Type Safety in Low-Level Code, published in volume 102 in Electronic Proceedings in Theoretical Computer Science (EPTCS), pages 73-87. Done together with Tjark and Marcus.
  copy: [pdf]

• Waiting for Locks: How Long Does It Usually Take?, published in LNCS volume 7437, pages 47-62. Done together with Christel, Marcus Daum, Benjamin, Hermann, Joachim, Sascha, Steffen and Marcus Völp.
  copy: [pdf]

• Proceedings of the 6th International Workshop on Systems Software Verification (SSV 2011), published as volume 24 of OpenAccess Series in Informatics (OASICS) by Schloss Dagstuhl. Done together with Jörg and Marco (editors).
  link: [online proceedings]

  The proceedings have previously appeared as Technical report TUD-FI11-02-August 2011 of TU Dresden.
  copy: [pdf]

• Performance issues of Selective Disclosure and Blinded Issuing Protocols on Java Card, published in the proceedings of the workshop in information security, theory and practices (WISTP 2009), LNCS volume 5746, pages 95-111. Done together with Bart Jacobs.
  copy: [ps.gz] [pdf]

• Preemption Abstraction: A Lightweight Approach to Modelling Concurrency, published in the Proceedings of the 14th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2009), LNCS 5825, pages 149-164. Done together with Erik, Alejandro, Marko and Sjaak.
  copy: [pdf]

• Formal Memory Models for the Verification of Low-Level Operating-System Code, published in the Journal of Automated Reasoning, volume 42, number 2-4. Done together with Tjark and Marcus.
  copy: [ps.gz] (apart from formatting and page numbering this version is identical with the one printed in the journal)

• Nova interface specification, Robin deliverable D12, also available as technical report ICIS-R08011 of the ICIS department. Done together with Tjark, Erik, Marko and Peter. See also my Robin page.
  copy: [ps.gz]

• Nova micro-hypervisor verification, Robin deliverable D13, with minor modifications also available as technical report ICIS-R08012 of the ICIS department. Done together with Tjark, Marcus, Erik, Marko and Peter. See also my Robin page.
  copy TR version: [ps.gz] (see my Robin page for the original deliverable)

• A Formal Model of Memory Peculiarities for the Verification of Low-Level Operating-System Code, published in the proceedings of the 3rd international workshop in Systems Software Verification (SSV08), Sydney, ENTCS volume 217, pages 79-96. Together with Tjark and Marcus.
  copy [ps.gz]

• Formal Methods in the Robin project: Specification and verification of the Nova microhypervisor, published in the proceedings of the C/C++ Verification workshop.
  copy: [a4 ps.gz]

• Olmar: manipulating C and C++ abstract syntax trees in Ocaml, published in the proceedings of the C/C++ Verification workshop.
  copy: [a4 ps.gz]

• Micro hypervisor verification: possible approaches and relevant properties, published in the proceedings of the NLUUG Voorjaarsconferentie 2007.
  copy: [a4 ps.gz]

• Specification and verification of the Nova microhypervisor, Robin D.6 deliverable. Together with Bart Jacobs, Erik Poll, Marko van Eekelen and Peter van Rossum.
  copy: [short version ps.gz] [complete version ps.gz]

• The VFiasco approach for a verified operating system, together with Michael, Proceedings of the 2nd ECOOP Workshop on Programm Languages and Operating Systems.
  copy: [a4 ps.gz]

• Verifying Duff's device: A simple compositional denotational semantics for Goto and computed jumps, submitted.
  copy: [ps.gz]

• Predicate and Relation Lifting for Parametric Algebraic Specifications, Proceedings of CMCS 04. ENTCS volume 106, pages 335-353.
  copy: [a4 ps.gz]

• The Semantics of C++ Data Types: Towards Verifying low-level System components, together with Michael. TPHOLs 2003, Emerging Trends Proceedings. Technical Report No. 187 Institut für Informatik Universität Freiburg.
  copy: [a4 ps.gz]

• Coalgebraic Methods for Object-Oriented Specification, PhD, TU Dresden. Download here.

• The Coalgebraic Class Specification Language CCSL -Syntax and Semantics-, TU Dresden technical report TUD-FI02-08-August 2002.
  copy [a4 2up ps.gz] [a4 ps.gz]

• Applying source-code verification to a microkernel, together with Michael Hohmuth and Shane G. Stephens. TU Dresden technical report TUD-FI02-03-März 2002.
  copy [a4.ps.gz]

  There is also a 5 page extended abstract, (published in the proceedings of the 10th ACM SIGOPS European Workshop, 2002):
  copy [a4-abstr.ps.gz]

• Greatest Bisimulations for Binary Methods, published in ENTCS Volume 65 (CMCS '02).
  This is a successor to my paper "Coalgebras for Binary Methods ..." describing two results about taking unions of bisimulations.
  Online material (formalisation in PVS) is available here.
  copy [a4.ps.gz]

• Assertional and Behavioural Refinement in Coalgebraic Specification together with Bart Jacobs.
  This is the paper for an invited talk of Bart. Unfortunately the organizers of that workshop or conference did not produce any proceedings...
  Section 6 contains a small case study on a transaction-commit mechanism in CCSL. See this page.
  copy [a4.ps.gz]

• Coalgebras for Binary Methods: Properties of Bisimulations and Invariants in Theoretical Informatics and Applications 35(1):83-111, (extended version of my CMCS '00 paper Coalgebras for Binary Methods)
  Online material (formalisation in PVS) is available here.
  copy [a4.ps.gz]

• VFiasco - Towards a Provably Correct Microkernel, Technical Report TUD-FI01-1 together with Hermann Härtig and Michael Hohmuth.
  copy [a4.ps.gz]

• The Coalgebraic Class Specification Language CCSL together with Jan Rothe and Bart Jacobs. Journal of Universal Computer Science 7(2):175-193.
  copy [full-paper.ps.gz] [extended-abstract.ps.gz]

• Case study in coalgebraic specification: Memory management in the Fiasco microkernel. Technical report TPG2/1/2000 of the SFB 358.
  The case study itself, with all necessary sources is online available.
  copy [paper.ps.gz]

• Coalgebras for Binary Methods, appeared in ENTCS Volume 33 (CMCS '00) (an extended version is available as Coalgebras for Binary Methods: Properties of Bisimulations and Invariants)
  Online material (formalisation in PVS) is available here.
  copy [paper-a4.ps.gz]

• Reasoning about Java Classes, together with Marieke, Bart, Joachim, Martijn and Uli (appeared in OOPSLA '98)
  copy [a4.ps.gz]

• Reasoning about Classes in Object-Oriented Languages: Logical Models and Tools, together with Marieke, Uli and Bart (appeared in ESOP '98)
  copy [a4.ps.gz]

• My Diploma [copy a4.ps.gz]

• My 4th year project [copy a4.ps.gz]

Home Science Overview All Publications Talks PhD CCSL Robin