Witnessing the elimination of magic wands.
Saved in:
| Title: | Witnessing the elimination of magic wands. |
|---|---|
| Authors: | Blom, Stefan1 s.c.c.blom@utwente.nl, Huisman, Marieke1 m.huisman@utwente.nl |
| Source: | International Journal on Software Tools for Technology Transfer. Nov2015, Vol. 17 Issue 6, p757-781. 25p. |
| Subjects: | Software verification, Computer operators, Server farms (Computer network management), Java programming language, Algorithms, Formal methods (Computer science), Hoare logic |
| Abstract: | This paper discusses static verification of programs that have been specified using separation logic with magic wands. Magic wands are used to specify incomplete resources in separation logic, i.e., if missing resources are provided, a magic wand allows one to exchange these for the completed resources. One of the applications of the magic wand operator is to describe loop invariants for algorithms that traverse a data structure, such as the imperative version of the tree delete problem (Challenge 3 from the VerifyThis@FM2012 Program Verification Competition), which is the motivating example for our work. Most separation logic-based static verification tools do not provide support for magic wands, possibly because validity of formulas containing the magic wand is, by itself, undecidable. To avoid this problem, in our approach the program annotator has to provide a witness for the magic wand, thus circumventing undecidability due to the use of magic wands. A witness is an object that encodes both instructions for the permission exchange that is specified by the magic wand and the extra resources needed during that exchange. We show how this witness information is used to encode a specification with magic wands as a specification without magic wands. Concretely, this approach is used in the VerCors tool set: annotated Java programs are encoded as Chalice programs. Chalice then further translates the program to BoogiePL, where appropriate proof obligations are generated. Besides our encoding of magic wands, we also discuss the encoding of other aspects of annotated Java programs into Chalice, and in particular, the encoding of abstract predicates with permission parameters. We illustrate our approach on the tree delete algorithm, and on the verification of an iterator of a linked list. [ABSTRACT FROM AUTHOR] |
| Copyright of International Journal on Software Tools for Technology Transfer is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) | |
| Database: | Engineering Source |
| FullText | Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 110204072 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: Witnessing the elimination of magic wands. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Blom%2C+Stefan%22">Blom, Stefan</searchLink><relatesTo>1</relatesTo><i> s.c.c.blom@utwente.nl</i><br /><searchLink fieldCode="AR" term="%22Huisman%2C+Marieke%22">Huisman, Marieke</searchLink><relatesTo>1</relatesTo><i> m.huisman@utwente.nl</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22International+Journal+on+Software+Tools+for+Technology+Transfer%22">International Journal on Software Tools for Technology Transfer</searchLink>. Nov2015, Vol. 17 Issue 6, p757-781. 25p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Software+verification%22">Software verification</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+operators%22">Computer operators</searchLink><br /><searchLink fieldCode="DE" term="%22Server+farms+%28Computer+network+management%29%22">Server farms (Computer network management)</searchLink><br /><searchLink fieldCode="DE" term="%22Java+programming+language%22">Java programming language</searchLink><br /><searchLink fieldCode="DE" term="%22Algorithms%22">Algorithms</searchLink><br /><searchLink fieldCode="DE" term="%22Formal+methods+%28Computer+science%29%22">Formal methods (Computer science)</searchLink><br /><searchLink fieldCode="DE" term="%22Hoare+logic%22">Hoare logic</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: This paper discusses static verification of programs that have been specified using separation logic with magic wands. Magic wands are used to specify incomplete resources in separation logic, i.e., if missing resources are provided, a magic wand allows one to exchange these for the completed resources. One of the applications of the magic wand operator is to describe loop invariants for algorithms that traverse a data structure, such as the imperative version of the tree delete problem (Challenge 3 from the VerifyThis@FM2012 Program Verification Competition), which is the motivating example for our work. Most separation logic-based static verification tools do not provide support for magic wands, possibly because validity of formulas containing the magic wand is, by itself, undecidable. To avoid this problem, in our approach the program annotator has to provide a witness for the magic wand, thus circumventing undecidability due to the use of magic wands. A witness is an object that encodes both instructions for the permission exchange that is specified by the magic wand and the extra resources needed during that exchange. We show how this witness information is used to encode a specification with magic wands as a specification without magic wands. Concretely, this approach is used in the VerCors tool set: annotated Java programs are encoded as Chalice programs. Chalice then further translates the program to BoogiePL, where appropriate proof obligations are generated. Besides our encoding of magic wands, we also discuss the encoding of other aspects of annotated Java programs into Chalice, and in particular, the encoding of abstract predicates with permission parameters. We illustrate our approach on the tree delete algorithm, and on the verification of an iterator of a linked list. [ABSTRACT FROM AUTHOR] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>Copyright of International Journal on Software Tools for Technology Transfer is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=110204072 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.1007/s10009-015-0372-3 Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 25 StartPage: 757 Subjects: – SubjectFull: Software verification Type: general – SubjectFull: Computer operators Type: general – SubjectFull: Server farms (Computer network management) Type: general – SubjectFull: Java programming language Type: general – SubjectFull: Algorithms Type: general – SubjectFull: Formal methods (Computer science) Type: general – SubjectFull: Hoare logic Type: general Titles: – TitleFull: Witnessing the elimination of magic wands. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Blom, Stefan – PersonEntity: Name: NameFull: Huisman, Marieke IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 11 Text: Nov2015 Type: published Y: 2015 Identifiers: – Type: issn-print Value: 14332779 Numbering: – Type: volume Value: 17 – Type: issue Value: 6 Titles: – TitleFull: International Journal on Software Tools for Technology Transfer Type: main |
| ResultId | 1 |
