Towards verified construction of correct and optimised GPU software

Marieke Huisman; Anton Wijs

doi:10.1145/3427761.3428344

Towards verified construction of correct and optimised GPU software

Marieke Huisman, Anton Wijs

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

69 Downloads (Pure)

Abstract

Techniques are required that support developers to produce GPU software that is both functionally correct and high-performing. We envision an integration of push-button formal verification techniques into a Model Driven Engineering workflow. In this paper, we present our vision on this topic, and how we plan to make steps in that direction in the coming five years.

Original language	English
Title of host publication	FTfJP 2020
Subtitle of host publication	Proceedings of the 22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs
Editors	Wytse Oortwijn
Publisher	Association for Computing Machinery
Pages	10-14
Number of pages	5
ISBN (Electronic)	9781450381864
DOIs	https://doi.org/10.1145/3427761.3428344
Publication status	Published - 23 Jul 2020
Event	22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2020 - Online Duration: 23 Jul 2020 → 23 Jul 2020 Conference number: 22

Workshop

Workshop	22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2020
Abbreviated title	FTfJP
Period	23/07/20 → 23/07/20

Keywords

Code generation
Formal verification
GPU software
Model transformation
22/2 OA procedure

Access to Document

10.1145/3427761.3428344

Huisman2020towardsFinal published version, 508 KBLicence: Taverne

Cite this

@inproceedings{d1a2a8feee9e4ad583793d2c39d1a0d0,

title = "Towards verified construction of correct and optimised GPU software",

abstract = "Techniques are required that support developers to produce GPU software that is both functionally correct and high-performing. We envision an integration of push-button formal verification techniques into a Model Driven Engineering workflow. In this paper, we present our vision on this topic, and how we plan to make steps in that direction in the coming five years. ",

keywords = "Code generation, Formal verification, GPU software, Model transformation, 22/2 OA procedure",

author = "Marieke Huisman and Anton Wijs",

year = "2020",

month = jul,

day = "23",

doi = "10.1145/3427761.3428344",

language = "English",

pages = "10--14",

editor = "Wytse Oortwijn",

booktitle = "FTfJP 2020",

publisher = "Association for Computing Machinery",

address = "United States",

note = "22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2020, FTfJP ; Conference date: 23-07-2020 Through 23-07-2020",

}

Huisman, M & Wijs, A 2020, Towards verified construction of correct and optimised GPU software. in W Oortwijn (ed.), FTfJP 2020: Proceedings of the 22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs. Association for Computing Machinery, pp. 10-14, 22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2020, 23/07/20. https://doi.org/10.1145/3427761.3428344

Towards verified construction of correct and optimised GPU software. / Huisman, Marieke; Wijs, Anton.
FTfJP 2020: Proceedings of the 22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs. ed. / Wytse Oortwijn. Association for Computing Machinery, 2020. p. 10-14.

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

TY - GEN

T1 - Towards verified construction of correct and optimised GPU software

AU - Huisman, Marieke

AU - Wijs, Anton

N1 - Conference code: 22

PY - 2020/7/23

Y1 - 2020/7/23

N2 - Techniques are required that support developers to produce GPU software that is both functionally correct and high-performing. We envision an integration of push-button formal verification techniques into a Model Driven Engineering workflow. In this paper, we present our vision on this topic, and how we plan to make steps in that direction in the coming five years.

AB - Techniques are required that support developers to produce GPU software that is both functionally correct and high-performing. We envision an integration of push-button formal verification techniques into a Model Driven Engineering workflow. In this paper, we present our vision on this topic, and how we plan to make steps in that direction in the coming five years.

KW - Code generation

KW - Formal verification

KW - GPU software

KW - Model transformation

KW - 22/2 OA procedure

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

U2 - 10.1145/3427761.3428344

DO - 10.1145/3427761.3428344

M3 - Conference contribution

AN - SCOPUS:85097780432

SP - 10

EP - 14

BT - FTfJP 2020

A2 - Oortwijn, Wytse

PB - Association for Computing Machinery

T2 - 22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2020

Y2 - 23 July 2020 through 23 July 2020

ER -

Towards verified construction of correct and optimised GPU software

Abstract

Workshop

Keywords

Access to Document

Other files and links

Fingerprint

Cite this