Thomas will develop methods that are capable of analysing the behaviour of software, while also producing a correctness certificate that carefully explains the analysis results. This requires extending advanced methods for efficient analysis with the capability to reason about such certificates and furthermore reduce their size. Independently verifying a certificate gives very high certainty about the correctness of the (safety-critical) software it describes.