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