Cooperative reasoning for automatic software verification

Separation logic was designed to simplify pointer program proofs. In terms of verification tools, the majority of effort has gone into developing light-weight analysis techniques for separation logic, such as shape analysis. Shape analysis ignores the content of data, focusing instead on how data is structured. While such light-weight properties can be extremely valuable, ultimately a more comprehensive level of specification is called for, i.e. correctness specifications. However, to verify such comprehensive specifications requires more heavy-weight analysis, i.e. theorem proving. We propose an integrated approach for the automatic verification of correctness specifications within separation logic. An approach which combines both light-weight and heavy-weight techniques is proposed. We are aiming for a cooperative style of integration, in which individual techniques combine their strengths, but crucially compensate for each other's weaknesses through the communication of partial results and failures. ©2007 ACM.