Sökning: onr:"swepub:oai:DiVA.org:kth-224402" >
An Abstraction Tech...
-
Oortwijn, W.
(författare)
An Abstraction Technique for Describing Concurrent Program Behaviour
- Artikel/kapitelEngelska2017
Förlag, utgivningsår, omfång ...
-
2017-12-15
-
Cham :Springer,2017
-
printrdacarrier
Nummerbeteckningar
-
LIBRIS-ID:oai:DiVA.org:kth-224402
-
https://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-224402URI
-
https://doi.org/10.1007/978-3-319-72308-2_12DOI
Kompletterande språkuppgifter
-
Språk:engelska
-
Sammanfattning på:engelska
Ingår i deldatabas
Klassifikation
-
Ämneskategori:ref swepub-contenttype
-
Ämneskategori:kon swepub-publicationtype
Anmärkningar
-
QC 20180316
-
This paper presents a technique to reason about functional properties of shared-memory concurrent software by means of abstraction. The abstract behaviour of the program is described using process algebras. In the program we indicate which concrete atomic steps correspond to the actions that are used in the process algebra term. Each action comes with a specification that describes its effect on the shared state. Program logics are used to show that the concrete program steps adhere to this specification. Separately, we also use program logics to prove that the program behaves as described by the process algebra term. Finally, via process algebraic reasoning we derive properties that hold for the program from its abstraction. This technique allows reasoning about the behaviour of highly concurrent, non-deterministic and possibly non-terminating programs. The paper discusses various verification examples to illustrate our approach. The verification technique is implemented as part of the VerCors toolset. We demonstrate that our technique is capable of verifying data- and control-flow properties that are hard to verify with alternative approaches, especially with mechanised tool support.
Ämnesord och genrebeteckningar
Biuppslag (personer, institutioner, konferenser, titlar ...)
-
Blom, S.
(författare)
-
Gurov, Dilian,1964-KTH,Teoretisk datalogi, TCS(Swepub:kth)u1jmacmb
(författare)
-
Huisman, M.
(författare)
-
Zaharieva-Stojanovski, M.
(författare)
-
KTHTeoretisk datalogi, TCS
(creator_code:org_t)
Sammanhörande titlar
-
Ingår i:9th International Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2017Cham : Springer, s. 191-2099783319723075
Internetlänk
Hitta via bibliotek
Till lärosätets databas