Gerwin Klein is working in formal software verification, interactive theorem proving, programming languages, and operating systems. He is a Principal Researcher at NICTA and Conjoint Associate Professor at the University of New South Wales in Sydney, Australia. He is coordinating NICTA's activities in Formal Methods. He received his PhD in Computer Science on Java Bytecode Verification from Technische Universität Munich in 2003 and has been working in the area of machine-checked formal proof in various projects since 1998.
When he is not developing proofs or software and not teaching students, he can be spotted enjoying martial arts, books, and cinema.