Formal Translation of Bytecode into BoogiePL. - Hermann Lehner; Peter Müller 001 (Bytecode@ETAPS, 2007)

Efficient Runtime Assertion Checking of Assignable Clauses with Datagroups. - Hermann Lehner; Peter Müller 001 (FASE, 2010)

A formal definition of JML in Coq and its application to runtime assertion checking. - Hermann Lehner (2011)

Resource-Rich versus Resource-Poor Assessment in Introductory Computer Science and its Implications on Models of Cognition: An in-Class Experimental Study. - Tobias Halbherr; Hermann Lehner; Manu Kapur (CogSci, 2019)