Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
An Abstraction Technique for Describing Concurrent Program Behaviour
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-0074-8786
Show others and affiliations
2017 (English)In: 9th International Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2017, Springer, 2017, Vol. 10712, p. 191-209Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Springer, 2017. Vol. 10712, p. 191-209
Series
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), ISSN 0302-9743 ; 10712
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:kth:diva-224402DOI: 10.1007/978-3-319-72308-2_12Scopus ID: 2-s2.0-85041435817ISBN: 9783319723075 OAI: oai:DiVA.org:kth-224402DiVA, id: diva2:1191191
Conference
9th International Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2017, Heidelberg, Germany, 22 July 2017 through 23 July 2017
Note

QC 20180316

Available from: 2018-03-16 Created: 2018-03-16 Last updated: 2018-03-16Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records BETA

Gurov, Dilian

Search in DiVA

By author/editor
Gurov, Dilian
By organisation
Theoretical Computer Science, TCS
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 3 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf