Page navigation: [goto list of talks] [goto list of papers] [goto lagacy stuff]

CCSL

Papers

• Performance issues of Selective Disclosure and Blinded Issuing Protocols on Java Card, to appear in the proceedings of the workshop in information security, theory and practices (WISTP 2009). Done together with Bart Jacobs.
  copy: [ps.gz] [ps] [pdf] [dvi.tar.gz]

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

• 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] [ps] [pdf] [dvi.tar.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] [ps] [pdf] [dvi.tar.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. Should appear in some ENTCS volume. Together with Tjark and Marcus.
  copy [ps.gz] [ps] [pdf]

• 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] [a4 ps]

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

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

• 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 recommended short version: [a4 ps.gz] [a4 ps]
  copy 29 pages appendices: [a4 ps.gz] [a4 ps]
  copy complete version: [a4 ps.gz] [a4 ps]

• 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 dvi] [a4 ps.gz] [a4 ps] [a4 pdf] [letter dvi] [letter ps.gz] [letter ps] [letter pdf]

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

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

• 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.
  Submitted version: [a4 ps] [a4 ps.gz] [a4 pdf] [letter ps] [letter ps.gz] [letter pdf]
  current version: [a4 ps] [a4 ps.gz] [a4 pdf] [letter ps] [letter ps.gz] [letter pdf]

• 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 2up ps] [a4 ps.gz] [a4 ps] [a4 dvi] [a4 pdf] [letter 2up ps.gz] [letter 2up ps] [letter ps.gz] [letter ps] [letter dvi] [letter pdf]

• 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] [a4.ps.gz] [a4.pdf] [letter.ps] [letter.ps.gz] [letter.pdf]

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

• 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] [a4.ps] [everything.tar.gz] [everything.tar]

• Assertional and Behavioural Refinement in Coalgebraic Specification together with Bart Jacobs, submitted.
  Section 6 of this paper contains a small case study on a transaction-commit mechanism in CCSL. See this page.
  copy [a4.ps.gz] [a4.ps] [everything.tar.gz] [everything.tar]

• Coalgebras for Binary Methods: Properties of Bisimulations and Invariants in Theoretical Informatics and Applications 25(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] [a4.ps] [everything.tar.gz] [everything.tar]

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

• 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] [full-paper.ps] [extended-abstract.ps.gz] [extended-abstract.ps]

• 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 [paper.ps] [everything-pvs-2.2.tar.gz] [everything-pvs-2.2.tar] (the work on the PVS 2.3 distribution is stuck because of problem #516)

• 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] [paper-a4.ps] [everything.tar.gz] [everything.tar]

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

• 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] [a4.ps]

Talks

• Micro-Hypervisor Verification: Possible Approaches and Relevant Properties, held at the spring conference of the dutch unix user group (NLUUG voorjaarsconferentie on May 10th in Ede, the Netherlands.
  copy [nluug.ps.gz] [nluug.ps]

• Well-behaved Memory on Top of Virtual Memory, virtual presentation on Nicta's International Workshop on System Verification, held on August 7 and 8 in Sydney.
  copy [wellbehavedmem.ps.gz] [wellbehavedmem.ps]

• CCSL: Coalgebras meet Algebras meet Higher-Order Logic, invited talk on the workshop Algorithms and Tools for Coinductive Reasoning, held on September 21st 2004 in Dresden.
  copy [ccsl.ps.gz] [ccsl.ps]

• Semantik hardware-naher Programme, held on July 12th 2004 in Karlsruhe.
  copy [system-level.ps.gz] [system-level.ps]
  The same talk was presented by Harvey Tuch at the NICTA Workshop on Operating Systems Verification on October 8th 2004 in Sydney.
  copy [system-level-en.ps.gz] [system-level-en.ps] (The english slides are slighly newer.)
  

• Koalgebren und Koinduktion: Eine leichte Einführung, held on July 13th 2004 in Karlsruhe.
  copy [coalg-intro.ps.gz] [coalg-intro.ps]
  

• Predicate and Relation Lifting for Parametric Algebraic Specifications, held at 7th International Workshop on Coalgebraic Methods in Computer Science on March 29th 2004 in Barcelona.
  copy [adt-lift.ps.gz] [adt-lift.ps]
  

• The Semantics of C++ Data Types: Towards Verifying low-level System Components, held in the emergency trends track of TPHOLs 2003 in September 2003 in Rome.
  copy [cpp-types.ps.gz] [cpp-types.ps] [cpp-types-poster.ps.gz] [cpp-types-poster.ps]
  

• The Coalgebraic Class Specification Language CCSL, held on July 25th 2003 in Bremen.
  copy [ccsl-bremen.ps.gz] [ccsl-bremen.ps]
  

• Coalgebraische Methoden für Objektorientierte Spezifikation, PhD defence talk, held on October 18th 2002 in Dresden.
  copy [promotion.ps.gz] [promotion.ps]
  

• Sicherheit mobiler Kommunikation, so-called scientific talk, replacing the PhD examination. Held on October 18th 2002 in Dresden.
  copy [kommunikation.ps.gz] [kommunikation.ps]
  

Some very old stuff

• Slides for the talk Rathen '97 [copy a4.ps.gz]

• Poster for the defence of the Graduiertenkolleg [copy a4.ps]

• My Diploma [copy a4.ps.gz]

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

Home Software Secrets Science