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