Cooperative reasoning for automatic software verification

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

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

Conference

Conference2nd Workshop on Automated Formal Methods
Abbreviated titleAFM'07
CountryUnited States
CityAtlanta, GA
Period6/11/076/11/07

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

Cite this