- Combining Mechanized Proofs and Model-Based Testing in
the Formal Analysis of a Hypervisor, published in the
proceedings of FM 2016 in LNCS 9995, pages 69-84.
Done together with the FireEye Formal Methods Team (Hanno, Juan, Ulrich,
Yoichi, Cesar, Keiko,
Jorge and Thomas)
and Jacek.
copy: [pdf]
- Formalizing Cut Elimination of Coalgebraic Logics in Coq
, published in the proceedings of the 22nd Conference on
Automated Reasoning with Analytic Tableaux and Related
Methods 2013,
LNAI
volume 8123,
pages 257-272.
copy paper:
[pdf]
Some documentation and the Coq sources of the formalization are
freely available here.
- A Probabilistic Quantitative Analysis of
Probabilistic-Write/Copy-Select,
published in the
proceedings of the Nasa Formal Methods Symposium 2013, LNCS
volume 7871, pages 307-321.
Done together with
Christel,
Benjamin,
Sascha,
Steffen and
Marcus Völp.
copy: [pdf]
- 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]