Hannes Mehnert

About

blog GitHub twitter hacker
PhD from ITU Copenhagen in 2013: Tools and Methods for Scalable Software Verification project (advisors Peter Sestoft and Lars Birkedal)
Currently research associate in the Rigorous Engineering for Mainstream Systems project (PI Peter Sewell)
eMail: hm519 at this domain name

Research Interest

Network protocols
Security
Operating systems
Software verification
Programming languages
Type Systems

Publications (reverse chronological order) (bibtex bibliography)

09/2016 Conex - establishing trust into data repositories by Hannes Mehnert and Louis Gesbert at OCaml 2016 (abstract)
02/2016 Not-quite-so-broken TLS 1.3 mechanised conformance checking by David Kaloper-Meršinjak and Hannes Mehnert at TLSv1.3 - Ready or Not? (TRON) slides
08/2015 Not-quite-so-broken TLS: lessons in re-engineering a security protocol specification and implementation by David Kaloper-Meršinjak, Hannes Mehnert, Anil Madhavapeddy and Peter Sewell at USENIX Security 2015 Supplementary material
12/2014 Nehmt euch die Kontrolle über eure privaten Daten zurück! by Hannes Mehnert in Jahrbuch Netzpolitik 2014 (Herausgeber: Markus Beckedahl, Anna Biselli, Andre Meister)
09/2014 Transport Layer Security purely in OCaml by Hannes Mehnert and David Kaloper at OCaml 2014 (abstract)
05/2014 Tool Demonstration: An IDE for Programming and Proving in Idris by Hannes Mehnert and David Christiansen at DTP 2014 (extended abstract accepted for presentation)
02/2014 Object Propositions by Ligia Nistor, Jonathan Aldrich, Stephanie Balzer, Hannes Mehnert at FM 2014 soundness proof composite proof technical report
12/2013 PhD dissertation Incremental Interactive Verification of the Correctness of Object-Oriented Software evaluation committee: Joseph Roland Kiniry, Marieke Huisman, Bart Jacobs; advisors: Peter Sestoft and Lars Birkedal (defense slides)
11/2013 Idris mode - Idris interaction with Emacs unpublished draft
06/2013 Das Curry-Buch by Hannes Mehnert, Jens Ohlig, Stefanie Schirmer (publisher: O'Reilly Germany) website pdf epub prc
05/2013 Kopitiam – a unified IDE for developing formally verified Java programs by Hannes Mehnert and Jesper Bengtson (ITU technical report 167)
03/2013 High-Level Abstractions for Safe Parallelism by Robert Bocchino, Jonathan Aldrich, Hannes Mehnert at WoDET 2013
06/2012 Encoding Featherweight Java with Assignment and Immutability using The Coq Proof Assistant by Julian Mackay, Hannes Mehnert, Alex Potanin, Lindsay Groves, Nicholas Cameron at FTfJP 2012 Coq formalization
05/2012 Verification of Snapshotable Trees using Access Permissions and Typestate by Hannes Mehnert and Jonathan Aldrich at TOOLS Java code
01/2012 Formalized Verification of Snapshotable Trees: Separation and Sharing by Hannes Mehnert, Filip Sieczkowski, Lars Birkedal, Peter Sestoft at VSTTE 2012 Coq formalization
04/2011 Kopitiam: modular incremental interactive full functional static verification of Java code by Hannes Mehnert at NFM 2011 slides screencast
10/2010 Extending Dylan's Type System for Better Type Inference and Error Detection by Hannes Mehnert at ILC 2010 source visualization front-end
04/2010 Relaxing Ownership with Immutability by Hannes Mehnert, Nicholas Cameron, Alex Potanin (Victoria University of Wellington technical report)
10/2009 Diplomarbeit: Extending Dylan's Type System for Better Type Inference and Error Detection source visualization front-end
03/2009 Automatically generated type-safe GTK+ binding for Dylan by Hannes Mehnert at ILC 2009
06/2007 Design and implementation of the middleware of Sputnik unpublished draft
04/2007 A Domain-Specific Language for manipulation of binary data in Dylan by Hannes Mehnert and Andreas Bogk at ILC 2007
10/2006 Nedap/Groenendaal ES3B voting computer - a security analysis by Rop Gonggrijp, Willem-Jan Hengeveld, Andreas Bogk, Dirk Engling, Hannes Mehnert, Frank Rieger, Pascal Scheffers, Barry Wels
08/2006 Secure networking by Andreas Bogk and Hannes Mehnert at 23rd Chaos Communication Congress
09/2005 International Conference on Functional Programming Programming Contest 2nd und Judge's Prize with the Dylan Hackers team (writeup local copy)

Selected projects

Not quite so broken protocol implementations
BTC Piñata
TLS demonstration server
(now maintained by Alexander Faithfull) Coqoon Eclipse plugin providing a feature-complete development environment for Coq proof scripts
(now maintained by Alexander Faithfull) Kopitiam Eclipse plugin for side-by-side development of Java code and Coq proofs (source on GitHub)
(no longer maintaining) Dylan compiler hacker and maintainer (Open Dylan) An object-centered dynamically typed programming language. Related to LISP, but with an ALGOL syntax and a clear separation of compile and run time. Dylan supports higher order functions, multiple inheritance, multiple dispatch, meta programming, exceptions, optional keyword arguments, …
There are two open source implementations, both written in Dylan: Gwydion Dylan (originally developed at CMU) which compiles Dylan to C, but has no thread support; and Open Dylan (formerly Functional Developer, developed at Harlequin), which compiles Dylan to either x86 assembly or C code. Open Dylan has an IDE (currently only on Windows) which supports debugging, REPL, etc.
(no longer maintained) Live control and data flow visualization for the Open Dylan compiler short demo Served as a debug tool for my Diplom thesis (to see what is going on during compilation) visualization front-end compiler source compiler source with advanced typing
(no longer maintained) Network night vision - network protocol analyzer and TCP/IP stack (including GUI)
(no longer maintained) KPortage - Gentoo package management KDE frontend
(no longer maintained) Buddha - DNS and DHCP configuration management (used in 2005/2006 for 4000 people network)
(no longer maintained) Sputnik - RFID tracking middleware (used in 2006/2007 to track 1000 people during 4 days at a conference)

Teaching (chronological order)

Fall 2007 Co-developed curriculum of "practical computer security" (MSc level, TU Berlin, Praktikum Rechnersicherheit)
Fall 2007 TA Methodical and practical foundations of computer science (BSc level, TU Berlin, Methodische und praktische Grundlagen der Informatik 4)
Fall 2010 TA Programs as data (BSc level, ITU Copenhagen)
Fall 2010 Programming languages seminar (MSc level, ITU Copenhagen)
Spring 2011: project: Development of a browser-based IDE (ITU Copenhagen)
Spring 2011: project: An Eclipse Plug-In for Coq (ITU Copenhagen)
Fall 2012: Programming languages seminar (MSc level, ITU Copenhagen)
Fall 2012: master thesis: Efficient Dynamic Method Dispatch on the Java Virtual Machine (ITU Copenhagen)
Spring 2013: Advanced Models and Programs (MSc level, ITU Copenhagen)
Spring 2013: project: Reverse engineering of the NemID client (ITU Copenhagen)