Zohar Manna, a pioneering computer science theorist and Stanford professor emeritus of computer science, died at his home in Netanya, Israel, on Aug. 30, surrounded by his family. He was 79.
Over a career spanning nearly 50 years, Manna pioneered two fields that were once at the theoretical edge of computing but which today help form the foundations for artificial intelligence and assure the reliability of extraordinarily complex software.
One of these fields was program synthesis, an important aspect of what is sometimes called automated reasoning. This is an approach to computation in which scientists design software that programs itself following strict rules of logic to provide a mathematical certainty of correct results. NASA used program synthesis to help generate the software that was used to analyze photographs of Saturn taken by the Cassini mission.
“Zohar was a profound thinker who laid the foundations for tools that are coming into widespread use today,” said Richard Waldinger, principal scientist at the Artificial Intelligence Laboratory at SRI International and Manna’s chief collaborator on program synthesis.
Starting with his PhD work and later in collaboration with now-deceased computer scientist Amir Pnueli, Manna helped to develop formal methods for software proof. This math-based approach stands in contrast to the typical way most software is written, tested and put into use, where unanticipated bugs must be corrected. Under the formal method of proof, software is subjected to logical and mathematical analysis before being released. The goal is to prove, mathematically, that the code will function flawlessly under any and all circumstances.
Thomas Henzinger, who earned his PhD under Manna and is today president of the Institute of Science and Technology Austria, said formal proofs are becoming increasingly necessary for assuring the safety of complex modern applications, which often involve what scientists call the “concurrent interaction” of many different subprograms and hardware routines. These concurrent interactions have increased to a point that it’s impossible to adequately test all the potential cross-influences using the traditional approach.
“If you open the automatic windows on a car the stereo may get louder,” Henzinger said, citing one harmless example of the unforeseen interactions that might arise in much more complex applications such as those in an autonomous car or air traffic control system.
Born in Haifa, Israel, in 1939, Manna earned his undergraduate and master’s degrees at Technion, the Israel Institute of Technology. Manna met his future wife, Nitza Kletchevsky, at a folk-dancing class in Haifa in 1959. The couple was married in 1963 and had four children, all of whom were at Manna’s bedside when he passed.
After serving for two years as a scientific programmer in the Israel Defense Forces, Manna attended Carnegie Mellon University, where he earned his PhD in computer science in 1968. That year, Manna began his first stint on the Stanford faculty as an assistant professor where, among other duties, he worked with artificial intelligence pioneer John McCarthy. In those pre-PowerPoint days, when academics used gesticulations and blackboards to illustrate their points, Manna developed a reputation as an engaging and energetic lecturer. “His friends called him the fastest chalk in the West,” Waldinger said.
Manna returned to Israel in 1972 to become a professor of applied mathematics at the Weizmann Institute. In 1975 he was recruited back to Stanford and became a full professor in 1978, dividing his time between Stanford and Weizmann until 1995, when he resigned the latter appointment. Manna continued as a Stanford professor until his retirement in 2010.
Manna authored or co-authored nine books and more than 125 scholarly articles. He trained 30 PhD students, many of whom went on to top academic posts in the United States, Europe, and Israel.
One of Manna’s earliest PhD students, Nachum Dershowitz, spoke at Manna’s 64th birthday celebration, attended by many of his protégés. “Each one of us has tales of his sound advice, sage counsel and joie de vivre,” Dershowitz said.
Stanford colleagues recall Manna’s devotion to his students, his affection for his peers and his endearing sense of humor.
“Zohar attracted the best students and brought out the best in everyone he worked with,” said David Dill, the Donald E. Knuth Professor in the School of Engineering, Emeritus.
Manna had “a hearty laugh, an instinct for procedural efficiency and a love of good food,” recalled John Mitchell, the Mary and Gordon Crary Family Professor in the School of Engineering.
Manna’s children recall a house full of guests, and Friday night family dinners and family camping trips. At blackjack tables, Manna was wont to test his mathematical genius by counting cards, a practice at which he got so good that he began getting blacklisted from casinos. “He laughed that it was one of his greatest achievements,” his son, Amit, recalls.
Among his many honors, Manna received the Bauer Prize from the Technical University of Munich, and an honorary doctorate from the French École Normale Supérieure de Cachan. Manna was a board member for the International Institute for Software Technology of the United Nations University.
Manna is survived by his wife, Nitza; his daughters Yonit, Hagit and Irit and his son, Amit; and five grandchildren.