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.
Keywords for this software
References in zbMATH (referenced in 7 articles , 1 standard article )
Showing results 1 to 7 of 7.
- Safari, Mohsen; Huisman, Marieke: Formal verification of parallel prefix sum and stream compaction algorithms in CUDA (2022)
- Oortwijn, Wytse; Gurov, Dilian; Huisman, Marieke: Practical abstractions for automated verification of shared-memory concurrency (2020)
- Müller, Peter (ed.); Schaefer, Ina (ed.): Principled software development. Essays dedicated to Arnd Poetzsch-Heffter on the occasion of his 60th birthday. Selected papers based on the presentations at the symposium, Kaiserslautern, Germany, November 2018 (2018)
- Oortwijn, Wytse; Blom, Stefan; Gurov, Dilian; Huisman, Marieke; Zaharieva-Stojanovski, Marina: An abstraction technique for describing concurrent program behaviour (2017)
- Müller, Peter; Schwerhoff, Malte; Summers, Alexander J.: Viper: a verification infrastructure for permission-based reasoning (2016)
- Amighi, Afshin; Blom, Stefan; Darabi, Saeed; Huisman, Marieke; Mostowski, Wojciech; Zaharieva-Stojanovski, Marina: Verification of concurrent systems with VerCors (2014)
- Blom, Stefan; Huisman, Marieke: The vercors tool for verification of concurrent programs (2014) ioport