Talks
- Combining Mechanized Proofs and Model-Based Testing in
the Formal Analysis of a Hypervisor,
presented in the security session of FM 2016 on November 11th, 2016 in Limassol, Cyprus.
[copy slides]
- Formalizing Cut Elimination of Coalgebraic Logics in Coq,
presented at the 22nd Conference on
Automated Reasoning with Analytic Tableaux and Related
Methods 2013 on September 17 in Nancy.
[copy slides]
Some documentation and the Coq sources of the formalization are
freely available here.
- Solving Operating-Systems Problems with Probabilistic
Model Checking, presentation for the
resilience path of cfaed (the Center for Advancing Electronics
Dresden), TU Dresden, Mai 3rd, 2013
[copy slides]
- Chiefly Symmetric: Results on the Scalability of
Probabilistic Model Checking for Operating-System Code ,
given at Systems Software Verification Converence (SSV 2012) on November
30, 2012 in Sydney
[copy slides]
- On the Use of Underspecified Data-Type Semantics for
Type Safety in Low-Level Code ,
given at Systems Software Verification Converence (SSV 2012) on November
29, 2012 in Sydney
[copy slides]
- Certified Verification of Security Properties for
Multicore Architectures ,
short presentation given on July 4th, 2012 at the expert
workshop on IT-security at the German Aerospace Center in
Köln.
[copy slides]
- Successful Diploma Writing (How to avoid leaving your
supervisor with bad memorys about you),
non-scientific talk given at the Echtzeit-AG on
July 13, 2012 in Dresden
[copy slides]
- Automatic Library Compilation and Proof-Tree
Visualisation for Coq Proof General, presentation at the
Third Coq
Workshop on August 26 2011 in Nijmegen.
[copy slides]
- Selective Disclosure Protocols on Java Card,
given at the Echtzeit-AG on March 3rd 2010 in Dresden.
[copy slides]
- Implementing Selective Disclosure Protocols on Java
Cards: A first experience report,
given at the Workshop
in Information Security Theory and Practices on September
3rd 2009 in Brussels
[copy slides]
- A Formal Model of Memory Peculiarities for the
Verification of Low-Level Operating-System Code,
given at the 3rd International Workshop on Systems Software Verification
(SSV 08) on February 25th 2008 in Sydney.
[copy slides]
- Microhypervisor Verification within the Robin Project,
given at the ICIS
colloquium on October 1st 2007 in Nijmegen.
[copy slides]
- Olmar: Manipulating C and C++ abstract syntax trees in Ocaml,
given at the C/C++
Verification Workshop on July 2nd 2007 in Oxford
[copy slides]
- Formal Methods in the Robin project: Specification and
verification of the Nova microhypervisor,
given at the C/C++
Verification Workshop on July 2nd 2007 in Oxford
[copy slides]
- Micro-Hypervisor Verification: Possible Approaches and
Relevant Properties,
given at the spring conference of the dutch unix user group (NLUUG
voorjaarsconferentie on May 10th 2007 in Ede, the
Netherlands.)
[copy slides]
- Verifying Duff's device: A simple compositional
denotational semantics for Goto and computed jumps,
given at the SoS
lunch colloquium on April 27th 2007 in Nijmegen.
[copy slides]
- Well-behaved Memory on Top of Virtual Memory,
virtual presentation on Nicta's International Workshop on System Verification,
given on August 7th and 8th 2006 in Sydney.
[copy slides]
- The VFiasco approach for a verified operating system,
given at the 2nd ECOOP Workshop on Programming Languages and
Operating Systems on July 26th 2005 in Glasgow.
[copy slides]
An expanded version of this talk has been presented on
September 30th 2005 in Nijmegen in the lunch colloquium of the
SOS group.
[copy slides]
- CCSL: Coalgebras meet Algebras meet Higher-Order
Logic, invited talk on the workshop Algorithms and Tools
for Coinductive Reasoning, given on September 21st 2004 in
Dresden.
[copy slides]
- Semantik hardware-naher Programme, given on July
12th 2004 in Karlsruhe.
[copy slides]
A slightly expanded version of the talk was presented by
Harvey Tuch at
the NICTA Workshop on Operating Systems Verification on
October 8th 2004 in Sydney.
[copy slides]
- Koalgebren und Koinduktion: Eine leichte Einführung,
given on July 13th 2004 in Karlsruhe.
[copy slides]
- Predicate and Relation Lifting for Parametric Algebraic
Specifications, given at 7th International Workshop on
Coalgebraic Methods in Computer Science on March 29th
2004 in Barcelona.
[copy slides]
- The Semantics of C++ Data Types: Towards Verifying
low-level System Components, given in the emergency trends
track of TPHOLs 2003 in September 2003 in Rome.
copy [copy slides]
[copy poster]
- The Coalgebraic Class Specification Language CCSL,
given on July 25th 2003 in Bremen.
[copy slides]
- Coalgebraische Methoden für Objektorientierte
Spezifikation, PhD defence talk, given on October 18th 2002
in Dresden.
[copy slides]
- Sicherheit mobiler Kommunikation, so-called
scientific talk, replacing the PhD examination. Given on October 18th 2002
in Dresden.
[copy slides]
- Greatest Bisimulations for Binary Methods,
given at 5th
International Workshop on Coalgebraic Methods in Computer
Science (CMCS 2002) on April 6th 2002 in Grenoble.
[copy slides]
- VFiasco - First Contact,
given at the Echtzeit-AG on February 6th 2002 in Dresden.
[copy slides]
- Coalgebras for Binary Methods,
given at the Workshop of the Graduiertenkolleg Specification of discrete processes and
systems of processes by operational models and logics
on February 2nd 2002 in Gohrisch.
[copy slides]
- Slides for the talk Rathen '97
[copy slides]
- Poster for the defence of the Graduiertenkolleg
[copy poster]
Home
Science Overview
All Publications
Talks
PhD
CCSL
Robin
last modified on
28 Nov 2016
by Hendrik