In Memoriam: Robin Milner and Amir Pnueli
May/June 2010 (VOL. 36, No. 3) pp. 5-5
/10/$31.00 © 2010 IEEE

Published by the IEEE Computer Society
In Memoriam: Robin Milner and Amir Pnueli
Bashar Nuseibeh
  Download Citation  
   
Download Content
 
PDFs Require Adobe Acrobat
 
In the last six months, the computing community, including software engineering, lost two of its greats: Robin Milner and Amir Pnueli. Both were Turing Award winners, and both contributed in fundamental ways to the foundations of software engineering. I had the privilege of meeting Robin Milner only, and my overriding memory is of a modest, gentle, approachable man, as open to other’s ideas as he was skilled at generating them. By all accounts, friends and colleagues speak equally warmly of Amir Pnueli—of his intellect, his wit, and his humor. Tributes to both individuals have been published widely both in the press and on the Internet.
I have included below short biographies of Professors Milner and Pnueli, extracted from their Web pages. I present these in the IEEE Transactions on Software Engineering as a small tribute to two outstanding computer scientists, and as an acknowledgment of their seminal contributions to our discipline.
Bashar Nuseibeh
Editor in Chief





Robin Milner (1934-2010) was appointed a professor of computer science at the University of Cambridge, United Kingdom, in 1995, and was head of the Computer Laboratory there from January 1996 to October 1999. Before that, he spent two years in the Artificial Intelligence Laboratory at Stanford University, then 22 years in the Computer Science Department at the University of Edinburgh, where, in 1986, he and colleagues founded the Laboratory for Foundations of Computer Science. He was elected a fellow of the Royal Society in 1988, and in 1991, he received the ACM’s Turing Award. Professor Milner’s intellectual legacy includes: a machine-assisted proof construction with the Logic for Computable Functions (LCF) approach, underpinning the HOL and Isabelle/HOL provers; the design and formal definition of programming languages, especially of Standard ML, including work on type safety, type inference, and module systems; models of concurrent computation, particularly with the CCS and Pi-Calculus process calculi and their theories of compositional reasoning; and, most recently, the bigraph model of mobile informatic processes with its applications to bioinformatics and pervasive computing. Some of this work is widely accessible through his books Communication and Concurrency (1989), Communicating and Mobile Systems (1999), and The Space and Motion of Communicating Agents (2009). Professor Milner received the BSc degree from the University of Cambridge in 1957, and was subsequently awarded some 10 Honorary Doctorates from universities around the world.





Amir Pnueli (1941-2009) completed the BSc degree in mathematics at the Technion, Haifa, and received the PhD degree in applied mathematics from the Weizmann Institute of Science, Israel, in 1967. He switched into computer science while a postdoctoral fellow at Stanford University and at the IBM T.J. Watson Research Center, Yorktown Heights, New York. He then returned to Israel to a position of a senior researcher in the Department of Applied Mathematics of the Weizmann Institute. In 1973, he moved to Tel-Aviv University, where he founded the Department of Computer Science and was its first chairman. In 1981, he returned to the Weizmann Institute as a professor of computer science. In 1997, he was appointed head of the “Minerva Center for Verification of Reactive Systems.” In 1999, he joined the Computer Science Department of New York University. Professor Pnueli was the 1996 recipient of the ACM Turing Award. He is primarily known for the introduction of temporal logic into computer science; his work on the application of temporal logic and similar formalisms for the specification and verification of reactive systems; the identification of the class of “Reactive Systems” as systems whose formal specification, analysis, and verification require a distinctive approach; and the development of a rich and detailed methodology, based on temporal logic, for the formal treatment of reactive system; extending this methodology into the realm of real-time systems; and, more recently, introducing into formal analysis the models of hybrid systems with appropriate extension of the temporal-logic based methodology. Besides his more theoretical work concerning a complete axiom system and proof theory for program verification by temporal logic, he also contributed to algorithmic research in this area. He developed a deductive system for linear-time temporal logic and model-checking algorithms for the verification of temporal properties of finite-state systems. Together with David Harel, he worked on the semantics and implementation of Statecharts, a visual language for the specification, modeling, and prototyping of reactive systems. This language has been applied to avionics, transport, and electronic hardware systems. Together with Zohar Manna, he was the author of a textbook series on Temporal Logic and its application to Reactive Systems (of which two volumes were published).

For information on obtaining reprints of this article, please send e-mail to: tse@computer.org.