Deductive Verification of SYCL in VerCors. Wittingen, E., Huisman, M., & Şakar, Ö. In Madeira, A. & Knapp, A., editors, Software Engineering and Formal Methods, pages 182–199, Cham, 2024. Springer Nature Switzerland. abstract bibtex SYCL is a C++ programming model for the development of heterogeneous programs. It uses the concept of kernels, where multiple instances of a computation are executed concurrently on a computing unit. This concurrency entails that the set of possible program behaviours can be of considerable size, which makes these programs error-prone. Formal verification could be used to ensure the correctness of all these possible program behaviours. However, there exist no formal verification tools for SYCL.
@InProceedings{10.1007/978-3-031-77382-2_11,
author="Wittingen, Ellen
and Huisman, Marieke
and {\c{S}}akar, {\"O}mer",
editor="Madeira, Alexandre
and Knapp, Alexander",
title="Deductive Verification of SYCL in VerCors",
booktitle="Software Engineering and Formal Methods",
year="2024",
publisher="Springer Nature Switzerland",
address="Cham",
pages="182--199",
abstract="SYCL is a C++ programming model for the development of heterogeneous programs. It uses the concept of kernels, where multiple instances of a computation are executed concurrently on a computing unit. This concurrency entails that the set of possible program behaviours can be of considerable size, which makes these programs error-prone. Formal verification could be used to ensure the correctness of all these possible program behaviours. However, there exist no formal verification tools for SYCL.",
isbn="978-3-031-77382-2"
}
Downloads: 0
{"_id":"2M5LNLMJSvmw678bv","bibbaseid":"wittingen-huisman-akar-deductiveverificationofsyclinvercors-2024","author_short":["Wittingen, E.","Huisman, M.","Şakar, Ö."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Wittingen"],"firstnames":["Ellen"],"suffixes":[]},{"propositions":[],"lastnames":["Huisman"],"firstnames":["Marieke"],"suffixes":[]},{"propositions":[],"lastnames":["Şakar"],"firstnames":["Ömer"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Madeira"],"firstnames":["Alexandre"],"suffixes":[]},{"propositions":[],"lastnames":["Knapp"],"firstnames":["Alexander"],"suffixes":[]}],"title":"Deductive Verification of SYCL in VerCors","booktitle":"Software Engineering and Formal Methods","year":"2024","publisher":"Springer Nature Switzerland","address":"Cham","pages":"182–199","abstract":"SYCL is a C++ programming model for the development of heterogeneous programs. It uses the concept of kernels, where multiple instances of a computation are executed concurrently on a computing unit. This concurrency entails that the set of possible program behaviours can be of considerable size, which makes these programs error-prone. Formal verification could be used to ensure the correctness of all these possible program behaviours. However, there exist no formal verification tools for SYCL.","isbn":"978-3-031-77382-2","bibtex":"@InProceedings{10.1007/978-3-031-77382-2_11,\nauthor=\"Wittingen, Ellen\nand Huisman, Marieke\nand {\\c{S}}akar, {\\\"O}mer\",\neditor=\"Madeira, Alexandre\nand Knapp, Alexander\",\ntitle=\"Deductive Verification of SYCL in VerCors\",\nbooktitle=\"Software Engineering and Formal Methods\",\nyear=\"2024\",\npublisher=\"Springer Nature Switzerland\",\naddress=\"Cham\",\npages=\"182--199\",\nabstract=\"SYCL is a C++ programming model for the development of heterogeneous programs. It uses the concept of kernels, where multiple instances of a computation are executed concurrently on a computing unit. This concurrency entails that the set of possible program behaviours can be of considerable size, which makes these programs error-prone. Formal verification could be used to ensure the correctness of all these possible program behaviours. However, there exist no formal verification tools for SYCL.\",\nisbn=\"978-3-031-77382-2\"\n}\n\n","author_short":["Wittingen, E.","Huisman, M.","Şakar, Ö."],"editor_short":["Madeira, A.","Knapp, A."],"key":"10.1007/978-3-031-77382-2_11","id":"10.1007/978-3-031-77382-2_11","bibbaseid":"wittingen-huisman-akar-deductiveverificationofsyclinvercors-2024","role":"author","urls":{},"metadata":{"authorlinks":{}},"html":""},"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/utwente-fmt/vercors-web/master/static/references.bib","dataSources":["cCvCnPTRQYq3qPe9y"],"keywords":[],"search_terms":["deductive","verification","sycl","vercors","wittingen","huisman","şakar"],"title":"Deductive Verification of SYCL in VerCors","year":2024}