Deductive techniques for model-based concurrency verification

Wytse Hendrikus Marinus Oortwijn

    Research output: ThesisPhD Thesis - Research UT, graduation UT

    135 Downloads (Pure)

    Abstract

    This thesis contributes formal techniques for verifying global behavioural properties of real-world concurrent software in a sound and practical manner.

    The first part of this thesis discusses how Concurrent Separation Logic (CSL) can be used to mechanically verify the parallel nested depth-first search (NDFS) model checking algorithm. This verification has been performed using VerCors. We also demonstrate how our mechanized correctness proof allows verifying various optimisations of parallel NDFS with only little extra effort.

    The second part contributes an abstraction technique for verifying global behavioural properties of shared-memory concurrent software. This abstraction technique allows specifying program behavior as a process-algebraic model, with an elegant algebraic structure. Furthermore, we extend CSL with logical primitives that allow one to prove that a program refines its process-algebraic specification. This abstraction technique is proven sound using Coq and is implemented in VerCors. We demonstrate our approach on various examples, including a real-world case study from industry that concerns safety-critical code.

    In part three, we lift our abstraction technique to the distributed case, by adapting it for verifying message passing concurrent software. This adaptation uses process-algebraic specifications to abstract the communication behavior of distributed agents. We also investigate how model checking of these specifications can soundly be combined with the deductive verification of the specified program.
    Original languageEnglish
    QualificationDoctor of Philosophy
    Awarding Institution
    • University of Twente
    Supervisors/Advisors
    • Huisman, Marieke , Supervisor
    Award date12 Dec 2019
    Place of PublicationEnschede
    Publisher
    Print ISBNs978-90-365-4898-4
    DOIs
    Publication statusPublished - 12 Dec 2019

    Fingerprint Dive into the research topics of 'Deductive techniques for model-based concurrency verification'. Together they form a unique fingerprint.

    Cite this