Sophie Lathouwers started as a PhD student on the Mercedes project. Sophie will investigate the automated generation of auxiliary annotations, which are needed for program verification in VerCors.