Practical Abstractions for Automated Verification of Shared-Memory Concurrency

Wytse Oortwijn, Dilian Gurov, Marieke Huisman

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

2 Citations (Scopus)

Abstract

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.
Original languageEnglish
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 21st International Conference, VMCAI 2020, New Orleans, LA, USA, January 16-21, 2020, Proceedings
EditorsDirk Beyer, Damien Zufferey
PublisherSpringer
Pages401-425
Number of pages25
ISBN (Electronic)978-3-030-39322-9
ISBN (Print)978-3-030-39321-2
DOIs
Publication statusPublished - 2020
Event21st International Conference on Verification,Model Checking, and Abstract Interpretation, VMCAI 2020 - JW Marriott New Orleans, New Orleans, United States
Duration: 19 Jan 202025 Jan 2020
Conference number: 21
https://popl20.sigplan.org/home/VMCAI-2020

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume11990

Conference

Conference21st International Conference on Verification,Model Checking, and Abstract Interpretation, VMCAI 2020
Abbreviated titleVMCAI 2020
CountryUnited States
CityNew Orleans
Period19/01/2025/01/20
Internet address

Fingerprint

Dive into the research topics of 'Practical Abstractions for Automated Verification of Shared-Memory Concurrency'. Together they form a unique fingerprint.

Cite this