Jean Pichon elaborates, ”we will clarify these poorly understood interfaces, and develop mathematically precise models of them, which we will thoroughly validate. We will phrase these models so that they can be used as reference test oracles by programmers to validate their designs. On top of these models, we will develop reasoning methods to mathematically capture the informal programming patterns that programmers rely on, and to show that they provide the desired guarantees. We will engage with industrial collaborators so that this work is integrated in the hardware architecture definitions and programming language standards.”

Jean Pichon joined the department on October 1, 2021 as a tenue track assistant professor in the Logic and Semantic research group. Prior to that, he was a at the Computer Laboratory of the University of Cambridge.