Gerwin Klein is working in formal software verification, interactive theorem proving, programming languages, and operating systems. He is a Chief Research Scientist at CSIRO's Data61 and Conjoint Professor at the University of New South Wales in Sydney, Australia. 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.