Vorträge
- Combining Mechanized Proofs and Model-Based Testing in
the Formal Analysis of a Hypervisor,
Vortrag auf FM 2016 am 11. November, 2016 in Limassol, Zypern.
[Präsentation]
- Formalizing Cut Elimination of Coalgebraic Logics in Coq,
Vortrag auf der 22. Conference für Automated Reasoning with Analytic Tableaux and Related
Methods 2013 am 17. September 2013 in Nancy.
[Präsentation]
Etwas Dokumentation und die Coq Quellen der Formalisierung sind
auf dieser Seiter
verfügbar (in english only).
- Solving Operating-Systems Problems with Probabilistic
Model Checking, Vortrag für den
Resilience Pfad des cfaed (Center for Advancing Electronics
Dresden), TU Dresden, 3. Mai, 2013
[Präsentation]
- Chiefly Symmetric: Results on the Scalability of
Probabilistic Model Checking for Operating-System Code ,
Vortrag auf der Systems Software Verification Converence
(SSV 2012) am 30. November 2012 in Sydney
[Präsentation]
- On the Use of Underspecified Data-Type Semantics for
Type Safety in Low-Level Code ,
Vortrag auf der Systems Software Verification Converence
(SSV 2012) am 29. November 2012 in Sydney
[Präsentation]
- 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.
[Präsentation]
- Successful Diploma Writing (How to avoid leaving your
supervisor with bad memorys about you),
nicht-wissenschaftlicher Vortrag in der Echtzeit-AG on
am 13. July 2012 in Dresden
[Präsentation]
- Automatic Library Compilation and Proof-Tree
Visualisation for Coq Proof General, Vortrag auf dem
Dritten Coq
Workshop am 26. August 2011 in Nijmegen.
[Präsentation]
- Selective Disclosure Protocols on Java Card,
gehalten in der Echtzeit-AG am 3. März 2010 in Dresden.
[Präsentation]
- Implementing Selective Disclosure Protocols on Java
Cards: A first experience report,
gehalten auf dem "Workshop
in Information Security Theory and Practices" am 3.
September 2009 in Brüssel.
[Präsentation]
- A Formal Model of Memory Peculiarities for the
Verification of Low-Level Operating-System Code,
gehalten auf dem 3. Internationalen Workshop zur Verifikation von Systemsoftware
(SSV 08) am 25 Februar 2008 in Sydney.
[Präsentation]
- Microhypervisor Verification within the Robin Project,
gehalten auf dem ICIS
Colloquium am 1. Oktober 2007 in Nijmegen.
[Präsentation]
- Olmar: Manipulating C and C++ abstract syntax trees in Ocaml,
gehalten auf dem C/C++
Verifikationsworkshop am 2. Juli 2007 in Oxford
[Präsentation]
- Formal Methods in the Robin project: Specification and
verification of the Nova microhypervisor,
gehalten auf dem C/C++
Verifikationsworkshop am 2. Juli 2007 in Oxford
[Präsentation]
- Micro-Hypervisor Verification: Possible Approaches and
Relevant Properties,
gehalten auf der Frühjarhrskonferenz der niederländischen Unixnutzergemeinschaft (NLUUG
voorjaarsconferentie am 10 Mai 2007 in Ede, in den Niederlanden.)
[Präsentation]
- Verifying Duff's device: A simple compositional
denotational semantics for Goto and computed jumps,
gehalten auf dem "SoS
lunch colloquium" am 27 April 2007 in Nijmegen.
[Präsentation]
- Well-behaved Memory on Top of Virtual Memory,
virtuelle Präsentation auf "Nicta's International Workshop on System
Verification",
gehalten am 7th August 2006 in Sydney.
[Präsentation]
- The VFiasco approach for a verified operating system,
gehalten auf dem 2. ECOOP Workshop für Programmiersprachen
und Betriebssysteme am 26. Juli 2005 in Glasgow.
[Präsentation]
Eine erweiterte Versions dieses Vortrages wurde am 30.
September 2005 in Nijmegen im Rahmen des SOS lunch
colloquium präsentiert.
[Präsentation]
- CCSL: Coalgebras meet Algebras meet Higher-Order
Logic, eingeladener Vortrag auf dem Workshop "Algorithms and Tools
for Coinductive Reasoning", gehalten am 21. September 2004 in
Dresden.
[Präsentation]
- Semantik hardware-naher Programme, gehalten am 12. Juli
2004 in Karlsruhe.
[Präsentation]
A leicht erweiterte Version dieses Vortrages wurde von Harvey Tuch beim
"NICTA Workshop on Operating Systems
Verification" am 8 Oktober 2004 in Sydney präsentiert.
[Präsentation]
- Koalgebren und Koinduktion: Eine leichte Einführung,
gehalten am 13. Juli 2004 in Karlsruhe.
[Präsentation]
- Predicate and Relation Lifting for Parametric Algebraic
Specifications, gehalten auf dem 7th International
Workshop für Coalgebraische Methoden in der Informatik
(CMCS '04) am 29 März
2004 in Barcelona.
[Präsentation]
- The Semantics of C++ Data Types: Towards Verifying
low-level System Components, gehalten im "Emergency trends
track" von TPHOLs 2003 im September 2003 in Rom.
[Präsentation]
[Poster]
- The Coalgebraic Class Specification Language CCSL,
gehalten am 25. Juli 2003 in Bremen.
[Präsentation]
- Coalgebraische Methoden für Objektorientierte
Spezifikation, Verteidigung meiner Doktorarbeit,
gehalten am 18. Oktober 2002
in Dresden.
[Präsentation]
- Sicherheit mobiler Kommunikation,
wissenschaftlicher Vortrag (als Ersatz des Rigorosoms),
gehaltem am 18. Oktober 2002
in Dresden.
[Präsentation]
- Greatest Bisimulations for Binary Methods,
gehalten auf dem 5. Internationalen Workshop für Coalgebraische Methoden in
der Informatik (CMCS 2002) am 6. April 2002 in Grenoble.
[Präsentation]
- VFiasco - First Contact,
gehalten auf der Echtzeit-AG am 6. Februar 2002 in Dresden.
[Präsentation]
- Coalgebras for Binary Methods,
gehalten auf dem Workshop des Graduiertenkolleg Spezifikation diskreter Prozesse und
Prozesssysteme durch operationelle Modelle und Logiken am
2. Februar 2002 in Gohrisch.
[Präsentation]
- Vortrag Rathen '97
[Präsentation]
- Poster für die Verteidigung des Graduiertenkollegs
[Poster]
Startseite
Wissenschaft Überblick
Alle Publikationen
Vorträge
Doktorarbeit
CCSL
Robin
geändert am
28 Nov 2016
von Hendrik