The VerCors Project: Setting Up Basecamp

A. Amighi, Stefan Blom, Marieke Huisman, M. Zaharieva

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

8 Citations (Scopus)
2 Downloads (Pure)

Abstract

This paper describes the first results and on-going work in the VerCors project. The VerCors project is about Verification of Concurrent Data Structures. Its goal is to develop a specification language and program logic for concurrent programs, and in particular for concurrent data structures, as these are the essential building blocks of many different concurrent programs. The program logic is based on our earlier work on permission-based separation logic for Java. This is an extension of Hoare logic that is particularly convenient to reason about concurrent programs. The paper first describes the tool set that is currently being built to support reasoning with this logic. It supports a specification language that combines features of separation logic with JML. For the verification, the program and its annotations are encoded into Chalice, and then we reuse the Chalice translation to Boogie to generate the proof obligations. Next, the paper describes our first results on data structure specifications. We use histories to keep track of the changes to the data structures, and we show how these histories allow us to derive other conclusions about the data structure implementations. We also discuss how we plan to reason about volatile variables, and how we will use this to verify lock-free data structures. Throughout the paper, we discuss our plans for future work within the VerCors project.
Original languageUndefined
Title of host publicationSixth Workshop Programming Languages meets Program Verification (PLPV 2012)
Place of PublicationNew York
PublisherAssociation for Computing Machinery (ACM)
Pages71-82
Number of pages12
ISBN (Print)978-1-4503-1125-0
DOIs
Publication statusPublished - 24 Jan 2012

Publication series

Name
PublisherACM

Keywords

  • IR-79578
  • METIS-296421
  • Concurrency
  • Separation Logic
  • CR-F.3.1
  • EWI-21412
  • EC Grant Agreement nr.: FP7/258405
  • CR-D.2.4
  • Permissions

Cite this

Amighi, A., Blom, S., Huisman, M., & Zaharieva, M. (2012). The VerCors Project: Setting Up Basecamp. In Sixth Workshop Programming Languages meets Program Verification (PLPV 2012) (pp. 71-82). New York: Association for Computing Machinery (ACM). https://doi.org/10.1145/2103776.2103785
Amighi, A. ; Blom, Stefan ; Huisman, Marieke ; Zaharieva, M. / The VerCors Project: Setting Up Basecamp. Sixth Workshop Programming Languages meets Program Verification (PLPV 2012). New York : Association for Computing Machinery (ACM), 2012. pp. 71-82
@inproceedings{f52ea079a2a4433696aba7c5c5d24651,
title = "The VerCors Project: Setting Up Basecamp",
abstract = "This paper describes the first results and on-going work in the VerCors project. The VerCors project is about Verification of Concurrent Data Structures. Its goal is to develop a specification language and program logic for concurrent programs, and in particular for concurrent data structures, as these are the essential building blocks of many different concurrent programs. The program logic is based on our earlier work on permission-based separation logic for Java. This is an extension of Hoare logic that is particularly convenient to reason about concurrent programs. The paper first describes the tool set that is currently being built to support reasoning with this logic. It supports a specification language that combines features of separation logic with JML. For the verification, the program and its annotations are encoded into Chalice, and then we reuse the Chalice translation to Boogie to generate the proof obligations. Next, the paper describes our first results on data structure specifications. We use histories to keep track of the changes to the data structures, and we show how these histories allow us to derive other conclusions about the data structure implementations. We also discuss how we plan to reason about volatile variables, and how we will use this to verify lock-free data structures. Throughout the paper, we discuss our plans for future work within the VerCors project.",
keywords = "IR-79578, METIS-296421, Concurrency, Separation Logic, CR-F.3.1, EWI-21412, EC Grant Agreement nr.: FP7/258405, CR-D.2.4, Permissions",
author = "A. Amighi and Stefan Blom and Marieke Huisman and M. Zaharieva",
note = "The 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '12 Philadelphia, PA, USA January 22-28, 2012",
year = "2012",
month = "1",
day = "24",
doi = "10.1145/2103776.2103785",
language = "Undefined",
isbn = "978-1-4503-1125-0",
publisher = "Association for Computing Machinery (ACM)",
pages = "71--82",
booktitle = "Sixth Workshop Programming Languages meets Program Verification (PLPV 2012)",
address = "United States",

}

Amighi, A, Blom, S, Huisman, M & Zaharieva, M 2012, The VerCors Project: Setting Up Basecamp. in Sixth Workshop Programming Languages meets Program Verification (PLPV 2012). Association for Computing Machinery (ACM), New York, pp. 71-82. https://doi.org/10.1145/2103776.2103785

The VerCors Project: Setting Up Basecamp. / Amighi, A.; Blom, Stefan; Huisman, Marieke; Zaharieva, M.

Sixth Workshop Programming Languages meets Program Verification (PLPV 2012). New York : Association for Computing Machinery (ACM), 2012. p. 71-82.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - The VerCors Project: Setting Up Basecamp

AU - Amighi, A.

AU - Blom, Stefan

AU - Huisman, Marieke

AU - Zaharieva, M.

N1 - The 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '12 Philadelphia, PA, USA January 22-28, 2012

PY - 2012/1/24

Y1 - 2012/1/24

N2 - This paper describes the first results and on-going work in the VerCors project. The VerCors project is about Verification of Concurrent Data Structures. Its goal is to develop a specification language and program logic for concurrent programs, and in particular for concurrent data structures, as these are the essential building blocks of many different concurrent programs. The program logic is based on our earlier work on permission-based separation logic for Java. This is an extension of Hoare logic that is particularly convenient to reason about concurrent programs. The paper first describes the tool set that is currently being built to support reasoning with this logic. It supports a specification language that combines features of separation logic with JML. For the verification, the program and its annotations are encoded into Chalice, and then we reuse the Chalice translation to Boogie to generate the proof obligations. Next, the paper describes our first results on data structure specifications. We use histories to keep track of the changes to the data structures, and we show how these histories allow us to derive other conclusions about the data structure implementations. We also discuss how we plan to reason about volatile variables, and how we will use this to verify lock-free data structures. Throughout the paper, we discuss our plans for future work within the VerCors project.

AB - This paper describes the first results and on-going work in the VerCors project. The VerCors project is about Verification of Concurrent Data Structures. Its goal is to develop a specification language and program logic for concurrent programs, and in particular for concurrent data structures, as these are the essential building blocks of many different concurrent programs. The program logic is based on our earlier work on permission-based separation logic for Java. This is an extension of Hoare logic that is particularly convenient to reason about concurrent programs. The paper first describes the tool set that is currently being built to support reasoning with this logic. It supports a specification language that combines features of separation logic with JML. For the verification, the program and its annotations are encoded into Chalice, and then we reuse the Chalice translation to Boogie to generate the proof obligations. Next, the paper describes our first results on data structure specifications. We use histories to keep track of the changes to the data structures, and we show how these histories allow us to derive other conclusions about the data structure implementations. We also discuss how we plan to reason about volatile variables, and how we will use this to verify lock-free data structures. Throughout the paper, we discuss our plans for future work within the VerCors project.

KW - IR-79578

KW - METIS-296421

KW - Concurrency

KW - Separation Logic

KW - CR-F.3.1

KW - EWI-21412

KW - EC Grant Agreement nr.: FP7/258405

KW - CR-D.2.4

KW - Permissions

U2 - 10.1145/2103776.2103785

DO - 10.1145/2103776.2103785

M3 - Conference contribution

SN - 978-1-4503-1125-0

SP - 71

EP - 82

BT - Sixth Workshop Programming Languages meets Program Verification (PLPV 2012)

PB - Association for Computing Machinery (ACM)

CY - New York

ER -

Amighi A, Blom S, Huisman M, Zaharieva M. The VerCors Project: Setting Up Basecamp. In Sixth Workshop Programming Languages meets Program Verification (PLPV 2012). New York: Association for Computing Machinery (ACM). 2012. p. 71-82 https://doi.org/10.1145/2103776.2103785