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.
|Title of host publication||AFM'07: 2nd Workshop on Automated Formal Methods|
|Number of pages||4|
|Publication status||Published - 2007|
|Event||2nd Workshop on Automated Formal Methods - Atlanta, GA, United States|
Duration: 6 Nov 2007 → 6 Nov 2007
|Conference||2nd Workshop on Automated Formal Methods|
|Period||6/11/07 → 6/11/07|