Johannes Kanig, senior software engineer at AdaCore and developer of the SPARK technology, received his PhD in formal verification from the University Paris-Sud, France.