kth.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • 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
Practical Abstractions for Automated Verification of Shared-Memory Concurrency
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.ORCID iD: 0000-0002-0074-8786
University of TwenteEnschedeThe Netherlands.
2020 (English)In: Lect. Notes Comput. Sci.: Verification, Model Checking, and Abstract Interpretation, Springer , 2020, p. 401-425Conference paper, Published paper (Refereed)
Abstract [en]

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 on expressivity and generality. This paper contributes a technique for verifying behavioural properties of concurrent and distributed programs that makes a trade-off between 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. 

Place, publisher, year, edition, pages
Springer , 2020. p. 401-425
Keywords [en]
Abstracting, Algebra, Automation, Economic and social effects, Software reliability, Automated verification, Deductive techniques, Distributed program, Distributed software, Leader election protocols, Multiple-case study, Program implementation, Verification techniques, Model checking
National Category
Algebra and Logic
Identifiers
URN: urn:nbn:se:kth:diva-274331DOI: 10.1007/978-3-030-39322-9_19ISI: 000655367300019Scopus ID: 2-s2.0-85079086514OAI: oai:DiVA.org:kth-274331DiVA, id: diva2:1442666
Conference
International Conference on Verification, Model Checking, and Abstract Interpretation 16 January 2020 through 21 January 2020
Note

QC 20200617

Available from: 2020-06-17 Created: 2020-06-17 Last updated: 2023-03-30Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopushttps://link.springer.com/chapter/10.1007%2F978-3-030-39322-9_19

Authority records

Gurov, Dilian

Search in DiVA

By author/editor
Gurov, Dilian
By organisation
Theoretical Computer Science, TCS
Algebra and Logic

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

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

Direct link
Cite
Citation style
  • apa
  • 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