@inproceedings{7e7d9f1f6e944f7fa094090c63a9d4ed,
title = "Formal Methods for GPGPU Programming: Is the Demand Met?",
abstract = "Over the years, researchers have developed many formal method tools to support software development. However, hardly any studies are conducted to determine whether the actual problems developers encounter are sufficiently addressed. For the relatively young field of GPU programming, we would like to know whether the tools developed so far are sufficient, or whether some problems still need attention. To this end, we first look at what kind of problems programmers encounter in OpenCL and CUDA. We gather problems from Stack Overflow and categorise them with card sorting. We find that problems related to memory, synchronisation of threads, threads in general and performance are essential topics. Next, we look at (verification) tools in industry and research, to see how these tools addressed the problems we discovered. We think many problems are already properly addressed, but there is still a need for easy to use sound tools. Alternatively, languages or programming styles can be created, that allows for easier checking for soundness.",
keywords = "Bugs, CUDA, Formal methods, GPGPU, GPU, OpenCL, Verification",
author = "{van den Haak}, Lars and Wijs, {Anton J.} and {van den Brand}, {Mark G.J.} and Marieke Huisman",
year = "2020",
doi = "10.1007/978-3-030-63461-2_9",
language = "English",
isbn = "9783030634605",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "160--177",
editor = "Brijesh Dongol and Elena Troubitsyna",
booktitle = "Integrated Formal Methods - 16th International Conference, IFM 2020, Proceedings",
address = "Germany",
note = "16th International Conference on Integrated Formal Methods, IFM 2020 ; Conference date: 16-11-2020 Through 20-11-2020",
url = {https://doi.org/10.1007/978-3-030-63461-2_9}
}

{"_id":"WKQ3f86frGEtPXzSQ","bibbaseid":"vandenhaak-wijs-vandenbrand-huisman-formalmethodsforgpgpuprogrammingisthedemandmet-2020","authorIDs":[],"author_short":["van den Haak , L.","Wijs, A.","van den Brand , M.","Huisman, M."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"Formal Methods for GPGPU Programming: Is the Demand Met?","abstract":"Over the years, researchers have developed many formal method tools to support software development. However, hardly any studies are conducted to determine whether the actual problems developers encounter are sufficiently addressed. For the relatively young field of GPU programming, we would like to know whether the tools developed so far are sufficient, or whether some problems still need attention. To this end, we first look at what kind of problems programmers encounter in OpenCL and CUDA. We gather problems from Stack Overflow and categorise them with card sorting. We find that problems related to memory, synchronisation of threads, threads in general and performance are essential topics. Next, we look at (verification) tools in industry and research, to see how these tools addressed the problems we discovered. We think many problems are already properly addressed, but there is still a need for easy to use sound tools. Alternatively, languages or programming styles can be created, that allows for easier checking for soundness.","keywords":"Bugs, CUDA, Formal methods, GPGPU, GPU, OpenCL, Verification","author":[{"propositions":["van den Haak"],"lastnames":[],"firstnames":["Lars"],"suffixes":[]},{"propositions":[],"lastnames":["Wijs"],"firstnames":["Anton J."],"suffixes":[]},{"propositions":["van den Brand"],"lastnames":[],"firstnames":["Mark G.J."],"suffixes":[]},{"firstnames":["Marieke"],"propositions":[],"lastnames":["Huisman"],"suffixes":[]}],"year":"2020","doi":"10.1007/978-3-030-63461-2_9","language":"English","isbn":"9783030634605","series":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","publisher":"Springer","pages":"160–177","editor":[{"firstnames":["Brijesh"],"propositions":[],"lastnames":["Dongol"],"suffixes":[]},{"firstnames":["Elena"],"propositions":[],"lastnames":["Troubitsyna"],"suffixes":[]}],"booktitle":"Integrated Formal Methods - 16th International Conference, IFM 2020, Proceedings","address":"Germany","note":"16th International Conference on Integrated Formal Methods, IFM 2020 ; Conference date: 16-11-2020 Through 20-11-2020","url":"https://doi.org/10.1007/978-3-030-63461-2_9","bibtex":"@inproceedings{7e7d9f1f6e944f7fa094090c63a9d4ed,\ntitle = \"Formal Methods for GPGPU Programming: Is the Demand Met?\",\nabstract = \"Over the years, researchers have developed many formal method tools to support software development. However, hardly any studies are conducted to determine whether the actual problems developers encounter are sufficiently addressed. For the relatively young field of GPU programming, we would like to know whether the tools developed so far are sufficient, or whether some problems still need attention. To this end, we first look at what kind of problems programmers encounter in OpenCL and CUDA. We gather problems from Stack Overflow and categorise them with card sorting. We find that problems related to memory, synchronisation of threads, threads in general and performance are essential topics. Next, we look at (verification) tools in industry and research, to see how these tools addressed the problems we discovered. We think many problems are already properly addressed, but there is still a need for easy to use sound tools. Alternatively, languages or programming styles can be created, that allows for easier checking for soundness.\",\nkeywords = \"Bugs, CUDA, Formal methods, GPGPU, GPU, OpenCL, Verification\",\nauthor = \"{van den Haak}, Lars and Wijs, {Anton J.} and {van den Brand}, {Mark G.J.} and Marieke Huisman\",\nyear = \"2020\",\ndoi = \"10.1007/978-3-030-63461-2_9\",\nlanguage = \"English\",\nisbn = \"9783030634605\",\nseries = \"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)\",\npublisher = \"Springer\",\npages = \"160--177\",\neditor = \"Brijesh Dongol and Elena Troubitsyna\",\nbooktitle = \"Integrated Formal Methods - 16th International Conference, IFM 2020, Proceedings\",\naddress = \"Germany\",\nnote = \"16th International Conference on Integrated Formal Methods, IFM 2020 ; Conference date: 16-11-2020 Through 20-11-2020\",\nurl = {https://doi.org/10.1007/978-3-030-63461-2_9}\n}\n\n\n","author_short":["van den Haak , L.","Wijs, A.","van den Brand , M.","Huisman, M."],"editor_short":["Dongol, B.","Troubitsyna, E."],"key":"7e7d9f1f6e944f7fa094090c63a9d4ed","id":"7e7d9f1f6e944f7fa094090c63a9d4ed","bibbaseid":"vandenhaak-wijs-vandenbrand-huisman-formalmethodsforgpgpuprogrammingisthedemandmet-2020","role":"author","urls":{"Paper":"https://doi.org/10.1007/978-3-030-63461-2_9"},"keyword":["Bugs","CUDA","Formal methods","GPGPU","GPU","OpenCL","Verification"],"metadata":{"authorlinks":{}},"downloads":0},"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/utwente-fmt/vercors-web/master/static/references.bib","creationDate":"2021-03-09T09:25:27.688Z","downloads":0,"keywords":["bugs","cuda","formal methods","gpgpu","gpu","opencl","verification"],"search_terms":["formal","methods","gpgpu","programming","demand","met","van den haak ","wijs","van den brand ","huisman"],"title":"Formal Methods for GPGPU Programming: Is the Demand Met?","year":2020,"dataSources":["2tJugFYAignELAmZo","zT4KxAXTKvhK2Hrr4","cCvCnPTRQYq3qPe9y"]}