Thomas Sternagel successfully defended his thesis on automation, formalization, and certification of confluence of conditional term rewrite systems. He will leave for industry in January.