Witnessing the elimination of magic wands

Stefan Blom, Marieke Huisman

Research output: Book/ReportReportProfessional

45 Downloads (Pure)

Abstract

This paper discusses the use and verification of 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. We show how the magic wand operator is suitable 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). Most separation-logic-based 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. 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
Place of PublicationEnschede
PublisherCentre for Telematics and Information Technology (CTIT)
Number of pages22
Publication statusPublished - 8 Nov 2013

Publication series

NameCTIT Technical Report Series
PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
No.TR-CTIT-13-22
ISSN (Print)1381-3625

Keywords

  • Separation Logic
  • EWI-23921
  • IR-87746
  • CR-D.2.4
  • Program Verification
  • METIS-300132

Cite this

Blom, S., & Huisman, M. (2013). Witnessing the elimination of magic wands. (CTIT Technical Report Series; No. TR-CTIT-13-22). Enschede: Centre for Telematics and Information Technology (CTIT).
Blom, Stefan ; Huisman, Marieke. / Witnessing the elimination of magic wands. Enschede : Centre for Telematics and Information Technology (CTIT), 2013. 22 p. (CTIT Technical Report Series; TR-CTIT-13-22).
@book{bb6b0f3fd4254a3fb37b6f03a7fa380d,
title = "Witnessing the elimination of magic wands",
abstract = "This paper discusses the use and verification of 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. We show how the magic wand operator is suitable 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). Most separation-logic-based 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. 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 = "Separation Logic, EWI-23921, IR-87746, CR-D.2.4, Program Verification, METIS-300132",
author = "Stefan Blom and Marieke Huisman",
year = "2013",
month = "11",
day = "8",
language = "Undefined",
series = "CTIT Technical Report Series",
publisher = "Centre for Telematics and Information Technology (CTIT)",
number = "TR-CTIT-13-22",
address = "Netherlands",

}

Blom, S & Huisman, M 2013, Witnessing the elimination of magic wands. CTIT Technical Report Series, no. TR-CTIT-13-22, Centre for Telematics and Information Technology (CTIT), Enschede.

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

Enschede : Centre for Telematics and Information Technology (CTIT), 2013. 22 p. (CTIT Technical Report Series; No. TR-CTIT-13-22).

Research output: Book/ReportReportProfessional

TY - BOOK

T1 - Witnessing the elimination of magic wands

AU - Blom, Stefan

AU - Huisman, Marieke

PY - 2013/11/8

Y1 - 2013/11/8

N2 - This paper discusses the use and verification of 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. We show how the magic wand operator is suitable 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). Most separation-logic-based 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. 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 the use and verification of 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. We show how the magic wand operator is suitable 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). Most separation-logic-based 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. 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 - Separation Logic

KW - EWI-23921

KW - IR-87746

KW - CR-D.2.4

KW - Program Verification

KW - METIS-300132

M3 - Report

T3 - CTIT Technical Report Series

BT - Witnessing the elimination of magic wands

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -

Blom S, Huisman M. Witnessing the elimination of magic wands. Enschede: Centre for Telematics and Information Technology (CTIT), 2013. 22 p. (CTIT Technical Report Series; TR-CTIT-13-22).