Cooperative reasoning for automatic software verification

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 languageEnglish
Title of host publicationAFM'07: 2nd Workshop on Automated Formal Methods
Number of pages4
Publication statusPublished - 2007
Event2nd Workshop on Automated Formal Methods - Atlanta, GA, United States
Duration: 6 Nov 20076 Nov 2007


Conference2nd Workshop on Automated Formal Methods
Abbreviated titleAFM'07
CountryUnited States
CityAtlanta, GA

Fingerprint Dive into the research topics of 'Cooperative reasoning for automatic software verification'. Together they form a unique fingerprint.

Cite this