Program Correctness by Transformation

Marieke Huisman; Stefan Blom; Saeed Darabi; Mohsen Safari

doi:10.1007/978-3-030-03418-4_22

Program Correctness by Transformation

Marieke Huisman, Stefan Blom, Saeed Darabi, Mohsen Safari

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

5 Citations (Scopus)

327 Downloads (Pure)

Abstract

Deductive program verification can be used effectively to verify high-level programs, but can be challenging for low-level, high-performance code. In this paper, we argue that compilation and program transformations should be made annotation-aware, i.e. during compilation and program transformation, not only the code should be changed, but also the corresponding annotations. As a result, if the original high-level program could be verified, also the resulting low-level program can be verified. We illustrate this approach on a concrete case, where loop annotations that capture possible loop parallelisations are translated into specifications of an OpenCL kernel that corresponds to the parallel loop. We also sketch how several commonly used OpenCL kernel transformations can be adapted to also transform the corresponding program annotations. Finally, we conclude the paper with a list of research challenges that need to be addressed to further develop this approach.

Original language	English
Title of host publication	Leveraging Applications of Formal Methods, Verification and Validation. Modeling
Subtitle of host publication	8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I
Editors	Tiziana Margaria, Bernhard Steffen
Place of Publication	Cham
Publisher	Springer
Pages	365-380
Number of pages	16
ISBN (Electronic)	978-3-030-03418-4
ISBN (Print)	978-3-030-03417-7
DOIs	https://doi.org/10.1007/978-3-030-03418-4_22
Publication status	Published - 2018
Event	8th International Symposium, ISoLA 2018 - Royal Apollonia Beach Hotel, Limassol, Cyprus Duration: 5 Nov 2018 → 9 Nov 2018 Conference number: 8 http://www.isola-conference.org/isola2018/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	11244
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	8th International Symposium, ISoLA 2018
Abbreviated title	ISoLA 2018
Country/Territory	Cyprus
City	Limassol
Period	5/11/18 → 9/11/18
Internet address	http://www.isola-conference.org/isola2018/

Access to Document

10.1007/978-3-030-03418-4_22

Program correctnessFinal published version, 863 KBLicence: Taverne

Cite this

Huisman, M., Blom, S., Darabi, S., & Safari, M. (2018). Program Correctness by Transformation. In T. Margaria, & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Modeling: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I (pp. 365-380). (Lecture Notes in Computer Science; Vol. 11244). Springer. https://doi.org/10.1007/978-3-030-03418-4_22

Huisman, Marieke ; Blom, Stefan ; Darabi, Saeed et al. / Program Correctness by Transformation. Leveraging Applications of Formal Methods, Verification and Validation. Modeling: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I. editor / Tiziana Margaria ; Bernhard Steffen. Cham : Springer, 2018. pp. 365-380 (Lecture Notes in Computer Science).

@inproceedings{dd7c6c42d2864b3a8f6cae25da1f5bd0,

title = "Program Correctness by Transformation",

abstract = "Deductive program verification can be used effectively to verify high-level programs, but can be challenging for low-level, high-performance code. In this paper, we argue that compilation and program transformations should be made annotation-aware, i.e. during compilation and program transformation, not only the code should be changed, but also the corresponding annotations. As a result, if the original high-level program could be verified, also the resulting low-level program can be verified. We illustrate this approach on a concrete case, where loop annotations that capture possible loop parallelisations are translated into specifications of an OpenCL kernel that corresponds to the parallel loop. We also sketch how several commonly used OpenCL kernel transformations can be adapted to also transform the corresponding program annotations. Finally, we conclude the paper with a list of research challenges that need to be addressed to further develop this approach.",

author = "Marieke Huisman and Stefan Blom and Saeed Darabi and Mohsen Safari",

year = "2018",

doi = "10.1007/978-3-030-03418-4_22",

language = "English",

isbn = "978-3-030-03417-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "365--380",

editor = "Tiziana Margaria and Bernhard Steffen",

booktitle = "Leveraging Applications of Formal Methods, Verification and Validation. Modeling",

address = "Germany",

note = "8th International Symposium, ISoLA 2018, ISoLA 2018 ; Conference date: 05-11-2018 Through 09-11-2018",

url = "http://www.isola-conference.org/isola2018/",

}

Huisman, M, Blom, S, Darabi, S & Safari, M 2018, Program Correctness by Transformation. in T Margaria & B Steffen (eds), Leveraging Applications of Formal Methods, Verification and Validation. Modeling: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I. Lecture Notes in Computer Science, vol. 11244, Springer, Cham, pp. 365-380, 8th International Symposium, ISoLA 2018, Limassol, Cyprus, 5/11/18. https://doi.org/10.1007/978-3-030-03418-4_22

Program Correctness by Transformation. / Huisman, Marieke; Blom, Stefan; Darabi, Saeed et al.
Leveraging Applications of Formal Methods, Verification and Validation. Modeling: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I. ed. / Tiziana Margaria; Bernhard Steffen. Cham: Springer, 2018. p. 365-380 (Lecture Notes in Computer Science; Vol. 11244).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Program Correctness by Transformation

AU - Huisman, Marieke

AU - Blom, Stefan

AU - Darabi, Saeed

AU - Safari, Mohsen

N1 - Conference code: 8

PY - 2018

Y1 - 2018

N2 - Deductive program verification can be used effectively to verify high-level programs, but can be challenging for low-level, high-performance code. In this paper, we argue that compilation and program transformations should be made annotation-aware, i.e. during compilation and program transformation, not only the code should be changed, but also the corresponding annotations. As a result, if the original high-level program could be verified, also the resulting low-level program can be verified. We illustrate this approach on a concrete case, where loop annotations that capture possible loop parallelisations are translated into specifications of an OpenCL kernel that corresponds to the parallel loop. We also sketch how several commonly used OpenCL kernel transformations can be adapted to also transform the corresponding program annotations. Finally, we conclude the paper with a list of research challenges that need to be addressed to further develop this approach.

AB - Deductive program verification can be used effectively to verify high-level programs, but can be challenging for low-level, high-performance code. In this paper, we argue that compilation and program transformations should be made annotation-aware, i.e. during compilation and program transformation, not only the code should be changed, but also the corresponding annotations. As a result, if the original high-level program could be verified, also the resulting low-level program can be verified. We illustrate this approach on a concrete case, where loop annotations that capture possible loop parallelisations are translated into specifications of an OpenCL kernel that corresponds to the parallel loop. We also sketch how several commonly used OpenCL kernel transformations can be adapted to also transform the corresponding program annotations. Finally, we conclude the paper with a list of research challenges that need to be addressed to further develop this approach.

UR - http://www.scopus.com/inward/record.url?scp=85056470177&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-03418-4_22

DO - 10.1007/978-3-030-03418-4_22

M3 - Conference contribution

SN - 978-3-030-03417-7

T3 - Lecture Notes in Computer Science

SP - 365

EP - 380

BT - Leveraging Applications of Formal Methods, Verification and Validation. Modeling

A2 - Margaria, Tiziana

A2 - Steffen, Bernhard

PB - Springer

CY - Cham

T2 - 8th International Symposium, ISoLA 2018

Y2 - 5 November 2018 through 9 November 2018

ER -

Huisman M, Blom S, Darabi S, Safari M. Program Correctness by Transformation. In Margaria T, Steffen B, editors, Leveraging Applications of Formal Methods, Verification and Validation. Modeling: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I. Cham: Springer. 2018. p. 365-380. (Lecture Notes in Computer Science). Epub 2018 Oct 29. doi: 10.1007/978-3-030-03418-4_22

Program Correctness by Transformation

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this