*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 23 Sep 2013 by Hendrik