Martín Abadi
Argentinischer Informatiker, der Sicherheitsprotokolle beweisbar machte und dieselbe Strenge anschließend auf maschinelles Lernen übertrug.
Die BAN-Logik (1989, mit Michael Burrows und Roger Needham) war das erste praktische formale Werkzeug, um zu begründen, was die Beteiligten eines Authentifizierungsprotokolls glauben dürfen. Mit Andrew Gordon entwickelte er 1997 den Spi-Kalkül, und mit Needham schrieb er die Liste vernünftiger Entwurfsregeln für Protokolle, die noch immer Fehler findet, die formale Methoden übersehen.
2005 führte er mit Kollegen von Microsoft Research die Control-Flow Integrity ein, die heute in Compilern und CPUs steckt. Bei Google war er Mitautor von TensorFlow und der 2016 veröffentlichten Methode für differentiell privates Deep Learning. Nur wenige haben so oft das Fachgebiet gewechselt, ohne je die Frage zu verlassen, was ein System tatsächlich garantiert.