Abstract
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.
Original language | English |
---|---|
Title of host publication | AFM'07: 2nd Workshop on Automated Formal Methods |
Pages | 51-54 |
Number of pages | 4 |
DOIs | |
Publication status | Published - 2007 |
Event | 2nd Workshop on Automated Formal Methods - Atlanta, GA, United States Duration: 6 Nov 2007 → 6 Nov 2007 |
Conference
Conference | 2nd Workshop on Automated Formal Methods |
---|---|
Abbreviated title | AFM'07 |
Country/Territory | United States |
City | Atlanta, GA |
Period | 6/11/07 → 6/11/07 |