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

Software Engineering and Technology

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

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 - Proceedings of the 22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2020, co-located with ECOOP 2020/SPLASH 2020
Editors	Wytse Oortwijn
Publisher	Association for Computing Machinery, Inc.
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, co-located with ECOOP 2020/SPLASH 2020 - Virtual, Online, United States Duration: 23 Jul 2020 → …

Conference

Conference	22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2020, co-located with ECOOP 2020/SPLASH 2020
Country/Territory	United States
City	Virtual, Online
Period	23/07/20 → …

Keywords

code generation
formal verification
GPU software
model transformation

Access to Document

10.1145/3427761.3428344

Cite this

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, FTfJP 2020, co-located with ECOOP 2020/SPLASH 2020 (pp. 10-14). Association for Computing Machinery, Inc.. https://doi.org/10.1145/3427761.3428344

@inproceedings{e152defd7b134657a25fa2d696ba7b92,

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",

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 - Proceedings of the 22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2020, co-located with ECOOP 2020/SPLASH 2020",

publisher = "Association for Computing Machinery, Inc.",

address = "United States",

note = "22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2020, co-located with ECOOP 2020/SPLASH 2020 ; Conference date: 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, FTfJP 2020, co-located with ECOOP 2020/SPLASH 2020. Association for Computing Machinery, Inc., pp. 10-14, 22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2020, co-located with ECOOP 2020/SPLASH 2020, Virtual, Online, United States, 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, FTfJP 2020, co-located with ECOOP 2020/SPLASH 2020. ed. / Wytse Oortwijn. Association for Computing Machinery, Inc., 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

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

UR - https://www.scopus.com/pages/publications/85097780432

U2 - 10.1145/3427761.3428344

DO - 10.1145/3427761.3428344

M3 - Conference contribution

AN - SCOPUS:85097780432

SP - 10

EP - 14

BT - FTfJP 2020 - Proceedings of the 22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2020, co-located with ECOOP 2020/SPLASH 2020

A2 - Oortwijn, Wytse

PB - Association for Computing Machinery, Inc.

T2 - 22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2020, co-located with ECOOP 2020/SPLASH 2020

Y2 - 23 July 2020

ER -

Towards verified construction of correct and optimised GPU software

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this