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.
Original languageUndefined
Pages (from-to)757-781
Number of pages25
JournalInternational journal on software tools for technology transfer
Volume17
Issue number6
DOIs
StatePublished - Nov 2015

Fingerprint

Specifications
Data structures
Mathematical operators

Keywords

  • program verificationseparation logicmagic wand
  • magic wand
  • EWI-26512
  • IR-98397
  • Separation Logic
  • METIS-315064
  • Program Verification

Cite this

Blom, Stefan; Huisman, Marieke / Witnessing the elimination of magic wands.

In: International journal on software tools for technology transfer, Vol. 17, No. 6, 11.2015, p. 757-781.

Research output: Scientific - peer-reviewArticle

@article{bcb261ee0d5643818bc219a14c568020,
title = "Witnessing the elimination of magic wands",
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.",
keywords = "program verificationseparation logicmagic wand, magic wand, EWI-26512, IR-98397, Separation Logic, METIS-315064, Program Verification",
author = "Stefan Blom and Marieke Huisman",
note = "Open Access",
year = "2015",
month = "11",
doi = "10.1007/s10009-015-0372-3",
volume = "17",
pages = "757--781",
journal = "International journal on software tools for technology transfer",
issn = "1433-2779",
publisher = "Springer Berlin Heidelberg",
number = "6",

}

Witnessing the elimination of magic wands. / Blom, Stefan; Huisman, Marieke.

In: International journal on software tools for technology transfer, Vol. 17, No. 6, 11.2015, p. 757-781.

Research output: Scientific - peer-reviewArticle

TY - JOUR

T1 - Witnessing the elimination of magic wands

AU - Blom,Stefan

AU - Huisman,Marieke

N1 - Open Access

PY - 2015/11

Y1 - 2015/11

N2 - 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.

AB - 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.

KW - program verificationseparation logicmagic wand

KW - magic wand

KW - EWI-26512

KW - IR-98397

KW - Separation Logic

KW - METIS-315064

KW - Program Verification

U2 - 10.1007/s10009-015-0372-3

DO - 10.1007/s10009-015-0372-3

M3 - Article

VL - 17

SP - 757

EP - 781

JO - International journal on software tools for technology transfer

T2 - International journal on software tools for technology transfer

JF - International journal on software tools for technology transfer

SN - 1433-2779

IS - 6

ER -