VerCors swMATH ID: 11259 Software Authors: Amighi, Afshin; Blom, Stefan; Darabi, Saeed; Huisman, Marieke; Mostowski, Wojciech; Zaharieva-Stojanovski, Marina Description: Verification of concurrent systems with VerCors. This paper presents the VerCors approach to verification of concurrent software. It first discusses why verification of concurrent software is important, but also challenging. Then it shows how within the VerCors project we use permission-based separation logic to reason about multithreaded Java programs. We discuss in particular how we use the logic to use different implementations of synchronisers in verification, and how we reason about class invariance properties in a concurrent setting. Further, we also show how the approach is suited to reason about programs using a different concurrency paradigm, namely kernel programs using the single instruction multiple data paradigm. Concretely, we illustrate how permission-based separation logic is suitable to verify functional correctness properties of OpenCL kernels. All verification techniques discussed in this paper are supported by the VerCors tool set. Homepage: http://link.springer.com/chapter/10.1007%2F978-3-319-07317-0_5 Related Software: Viper; Dafny; Boogie; GPUVerify; z3; Why3; Frama-C; Smallfoot; VeriFast; Chalice; VCC; Spec#; CUDA; Coq; JML; SIMPLIFY; Eiffel; Nagini; KeY; GKLEE Cited in: 10 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Verification of concurrent systems with VerCors. Zbl 1445.68131Amighi, Afshin; Blom, Stefan; Darabi, Saeed; Huisman, Marieke; Mostowski, Wojciech; Zaharieva-Stojanovski, Marina 2014 all top 5 Cited by 21 Authors 5 Huisman, Marieke 3 Oortwijn, Wytse 2 Blom, Stefan 2 Gurov, Dilian 2 Safari, Mohsen 2 Zaharieva-Stojanovski, Marina 1 Amighi, Afshin 1 Darabi, Saeed 1 Eilers, Marco 1 Groves, Lindsay J. 1 Hobor, Aquinas 1 Leow, Wei Xiang 1 Meier, Severin 1 Mohan, Anshuman 1 Mostowski, Wojciech I. 1 Müller, Peter 1 Pearce, David J. 1 Schaefer, Ina 1 Schwerhoff, Malte 1 Summers, Alexander J. 1 Utting, Mark Cited in 2 Serials 1 Theoretical Computer Science 1 Journal of Automated Reasoning Cited in 3 Fields 10 Computer science (68-XX) 2 Mathematical logic and foundations (03-XX) 1 General and overarching topics; collections (00-XX) Citations by Year