CAV Award 2016

The CAV Award 2016 was presented today to Josh Berdine, Cristiano Calcagno, Dino Distefano, Samin Ishtiaq, Peter O'Hearn, John Reynolds, and Hongseok Yang for "the development of Separation Logic and for demonstrating its applicability in the automated verification of programs that mutate data structures." This is the second major award that is given for work on Separation Logic in the space of roughly a week. Indeed, Steve Brookes and Peter O'Hearn received the 2016 Gödel Prize last week at ICALP 2016 for their invention of Concurrent Separation Logic. (The retrospective article describing Concurrent Separation Logic starts on page 47.)

The award recipients are honoured for the development of the theory of Separation Logic, which includes the key notion of separating conjunction, the work showing its applicability in the analysis of non-trivial programs, and the tool development that culminated in Facebook Infer.

Congratulations to the award recipients!

Those interested in learning about Separation Logic can consult, for instance, the following resources by Peter O'Hearn:

• A Primer on Separation Logic (and Automatic Program Verification and Analysis).
• Tutorial on Separation Logic. (slides)

Enjoy!