Verification of concurrent systems with VerCors
| Autor: | Amighi, Afshin, Blom, Stefan, Darabi, Saeed, Huisman, Marieke, Mostowski, Wojciech, Zaharieva-Stojanovski, Marina, Bernardo, Marco, Damiani, Ferruccio, Hähnle, Reiner, Broch Johnsen, Einar, Schaefer, Ina |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2014 |
| Předmět: |
Correctness
Java Computer science Concurrency CR-D.2.4 VerCors tool 02 engineering and technology Separation logic Permission computer.software_genre Global memory Software 020204 information systems Software verification 0202 electrical engineering electronic engineering information engineering EC Grant Agreement nr.: FP7/2007-2013 Implementation computer.programming_language Java modeling language Class invariant business.industry Programming language 020207 software engineering EC Grant Agreement nr.: FP7/258405 Concurrent program Class invariants business computer Concurrent system EC Grant Agreement nr.: FP7/287767 Java Modeling Language |
| Zdroj: | Formal Methods for Executable Software Models: 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, 172-216 STARTPAGE=172;ENDPAGE=216;TITLE=Formal Methods for Executable Software Models Lecture Notes in Computer Science ISBN: 9783319073163 SFM |
| ISSN: | 0302-9743 |
| DOI: | 10.1007/978-3-319-07317-0_5 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|