2016 Computer-Aided Verification Award

PARIS - Aug. 11, 2016 - PRLog -- CAV Award Announcement

The annual CAV (Computer-Aided Verification) Award recognizes a specific fundamental contribution or a series of outstanding contributions to computer-aided verification. The CAV award was established in 2008 by the steering committee of the CAV conference, which is the premier international event for reporting research on computer-aided verification, a sub-discipline of Computer Science that is concerned with ensuring that software and hardware systems operate correctly and reliably.

The 2016 CAV Award was given on July 21, 2016, at the 28th annual CAV conference held in Toronto, to

Josh Berdine, Cristiano Calcagno, Dino Distefano, Samin Ishtiaq, Peter O'Hearn, John Reynolds, and Hongseok Yang

for their pioneering work on "Separation Logic". The award citation acknowledges these researchers

"For the development of Separation Logic and for demonstrating its applicability in the automated verification of programs that mutate data structures".

The Award-Winning Contribution

Separation Logic is an extension of Hoare logic that allows reasoning about heap structures and pointer manipulation. The heap is the key aspect of imperative programs that makes their verification difficult, as compared to hardware designs or functional programs, especially, compositional reasoning about heap manipulating programs is particularly hard. Separation Logic provides the fundamental paradigm for achieving that, especially by introducing the crucial concept of the "separating conjunction". This was a real breakthrough that changed our way of thinking, and opened the door to a wide field of research that lead to the development of efficient verification tools for heap manipulating programs.

Separation Logic has been developed in a series of papers published between the years of 2000 to 2002, co-authored by Peter O'Hearn, John Reynolds, Samin Ishtiaq, and Hongseok Yang. This fundamental work was building on early work by Burstall in early 70's and by O'Hearn and Pym in late 90's on Bunched Logic.

Then, after the discovery of the logic, a team formed by Josh Berdine, Cristiano Calcagno, Dino Distefano, Peter O'Hearn and Hongseok Yang, undertook the challenge of demonstrating the use of Separation Logic in practice. This group of researchers developed a series of prototype tools for automated program verification exploiting Separation Logic (tools such as Space Invader and Smallfoot), and applied these tools successfully to significant industrial-size case studies. The design of these tools was based on new decision procedures for useful fragments of the logic as well as on efficient techniques for abstract program analysis (using abstract interpretation and) partly building on the principles of the "Shape Analysis" defined by Sagiv, Reps and Wilhelm, and introducing the key concept of bi-abduction. The work of this team was absolutely crucial in making separation logic very popular in our research community.

More generally, the work of the winners of 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 research around Separation Logic is still very active. 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. Other examples of the impact of Separation Logic are the SLAyer tool developed at Microsoft, which was applied there to device drivers, and the Infer tool developed and currently used at Facebook for the verification of mobile applications.

Bibliography:

• John Reynolds: Intuitionistic Reasoning about Shared Mutable Data Structure. 1999 Oxford-Microsoft Symposium in Honour of Sir Tony Hoare.
• Samin Ishtiaq, Peter O'Hearn: BI as an Assertion Language for Mutable Data Structures. POPL 2001.
• Peter O'Hearn, John Reynolds, Hongseok Yang: Local reasoning about Programs that Alter Data Structures. Invited paper, CSL'01, LNCS 2142.
• Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn: Symbolic Execution with Separation Logic. APLAS 2005, LNCS 3780.
• Dino Distefano, Peter W. O'Hearn, Hongseok Yang: A Local Shape Analysis Based on Separation Logic. TACAS 2006, LNCS 3920.
• Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang: Compositional shape analysis by means of bi-abduction. POPL 2009.

CAV Award web site: http://i-cav.org/cav-award