Computer-Aided Verification Award Honors Reynolds

Late Professor Cited for Pioneering Work on Separation Logic

Wednesday, August 10, 2016 - by Byron Spice

The late John C. Reynolds is one of a group of scientists awarded the 2016 Computer-Aided Verification (CAV) Award for pioneering work on separation logic.

The late John C. Reynolds is one of a group of scientists awarded the 2016 Computer-Aided Verification (CAV) Award for pioneering work on separation logic, an influential framework for reasoning about computer programs and a very active area of research.

The CAV Award, presented at the International Conference on Computer-Aided Verification last month in Toronto, cited the group "for the development of separation logic and for demonstrating its applicability in the automated verification of programs that mutate data structures."

Separation logic supports local reasoning, in which specifications and proofs of a program component mention only the portion of memory used by the component, rather than the entire global state of the system. This work forms the basis for automated tools for program analysis, capable of dealing with software running on parallel processors.

In addition to Reynolds, a longtime Computer Science Department faculty member who died in 2013, the group of honorees includes Josh Berdine, Cristiano Calcagno, Dino Distefano, Samin Ishtiaq, Peter O'Hearn and Hongseok Yang.

O'Hearn, engineering manager at Facebook and professor of computer science at University College London, was a friend and close colleague of Reynolds. Earlier this year, O'Hearn shared the 2016 Gödel Prize with Stephen Brookes, professor of computer science, for inventing concurrent separation logic.

According to the CAV award committee, Reynolds, O'Hearn, Ishtiaq and Yang developed the concept of separation logic in a series of papers from 2000 to 2002, while Berdine, Calcagno, Distefano, O'Hearn and Yang demonstrated the use of separation logic in practice.

"The work of the winners of the 2016 CAV Award had an important and deep impact on our community and is certainly among the major contributions to the area of formal methods and automated verification in the last two decades," the award committee stated in a news release. "Following the work initiated by the group of awardees, many researchers are nowadays working on both fundamental and practical issues related to separation logic and its use in efficient verification tools."

For more information, Contact:
Byron Spice | 412-268-9068 | bspice@cs.cmu.edu