Cousot, Patrick

Patrick Cousot

Professor of Computer Science

Patrick received the Doctor Engineer degree in Computer Science (1974) and the Doctor ès Sciences degree in Mathematics (1978) from the University Joseph Fourier of Grenoble, France.  Before coming to NYU in 2008, he was Professor at the École Normale Supérieure, the École Polytechnique, and the University of Metz, France.

Professor Cousot is one of the top leaders worldwide in the formal mathematical methods, and is the inventor, with Radhia Cousot, of “abstract interpretation,” a fundamental, general, and unifying theory of sound abstraction and approximation of mathematical structures that has had a tremendous influence on the field.  Myriad aspects of modern life depend on complex software – much of which has many “bugs.”  Professor Cousot's work provides tools to analyze software to automatically establish or verify the absence of errors in the software.  In addition to his fundamental theoretical contributions in this area, Professor Cousot has made very important practical contributions, particularly, his demonstration of the absence of run-time errors in the primary flight control software of the Airbus A340.

Abstract interpretation was introduced in the seminal 1977 paper, “Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints.”  This paper now has over 4500 citations, making it one of the most highly cited papers in computer science generally and in formal methods in particular.  The ideas have proven to be remarkably versatile: many “new” techniques can be shown to be special cases of the general abstract interpretation framework.  More importantly, recasting ideas in this framework immediately provides a host of insights as the abstract interpretation framework is well-developed, theoretically rich, and has been shown effective in many practical contexts.  In November 2003, the static analyzer Astrée (a tool based on abstract interpretation and developed under the leadership of Patrick Cousot) achieved a landmark verification milestone by successfully and automatically proving the absence of run-time errors in the primary flight control software of the Airbus A340 fly-by-wire system, a program consisting of 132,000 lines of computer code.  The ability of abstract interpretation to scale where other techniques (such as model checking) do not has led to a surge in interest in and uses of the technique. Today, abstract interpretation is one of the three pillars of formal methods become (along with model checking and theorem proving)

In recognition of his work, Cousot was awarded the Silver Medal of the CNRS (1999), a honorary doctorate from the Fakultät Mathematik und Informatik of the Universität des Saarlandes (2001), the Grand Prix of Computer Science and its Applications of the EADS Corporate Research Foundation attributed by the French Academy of Sciences (2006), a Humboldt Research Award (2008), the ACM SIGPLAN Programming Languages Achievement Award (2013), and most recently, with Radhia Cousot, the 2014 Harlan D. Mills Award (2014) of the IEEE Computer Society.