Search: id:"swepub:oai:DiVA.org:kth-278787" >
An Abstraction Tech...
An Abstraction Technique for Verifying Shared-Memory Concurrency
-
- Oortwijn, Wytse (author)
- Swiss Fed Inst Technol, Dept Comp Sci, CH-8092 Zurich, Switzerland.
-
- Gurov, Dilian, 1964- (author)
- KTH,Teoretisk datalogi, TCS
-
- Huisman, Marieke (author)
- Univ Twente, Formal Methods & Tools, NL-7500 AE Enschede, Netherlands.
-
Swiss Fed Inst Technol, Dept Comp Sci, CH-8092 Zurich, Switzerland Teoretisk datalogi, TCS (creator_code:org_t)
- 2020-06-05
- 2020
- English.
-
In: Applied Sciences. - : MDPI AG. - 2076-3417. ; 10:11
- Related links:
-
https://doi.org/10.3...
-
show more...
-
https://www.mdpi.com...
-
https://urn.kb.se/re...
-
https://doi.org/10.3...
-
show less...
Abstract
Subject headings
Close
- Modern concurrent and distributed software is highly complex. Techniques to reason about the correct behaviour of such software are essential to ensure its reliability. To be able to reason about realistic programs, these techniques must be modular and compositional as well as practical by being supported by automated tools. However, many existing approaches for concurrency verification are theoretical and focus primarily on expressivity and generality. This paper contributes a technique for verifying behavioural properties of concurrent and distributed programs that balances expressivity and usability. The key idea of the approach is that program behaviour is abstractly modelled using process algebra, and analysed separately. The main difficulty is presented by the typical abstraction gap between program implementations and their models. Our approach bridges this gap by providing a deductive technique for formally linking programs with their process-algebraic models. Our verification technique is modular and compositional, is proven sound with Coq, and has been implemented in the automated concurrency verifier VerCors. Moreover, our technique is demonstrated on multiple case studies, including the verification of a leader election protocol.
Subject headings
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Keyword
- concurrency verification
- program logics
- process algebra
- code verification
- abstraction
Publication and Content Type
- ref (subject category)
- art (subject category)
Find in a library
To the university's database