Skip to main content


Complx: A verification framework for concurrent imperative programs


Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Rizkallah Christine and Joseph Tuong


University of Pennsylvania



We propose a concurrency reasoning framework for imperative programs, based on the Owicki-Gries (OG) foundational shared-variable concurrency method. Our framework combines the approaches of Hoare-Parallel, a formalisation of OG in Isabelle/HOL for a simple while-language, and Simpl , a generic imperative language embedded in Isabelle/HOL, allowing formal reasoning on C programs. We define the C OMPLX language, extending the syntax and semantics of S IMPL with support for parallel composition and synchronisation. We additionally define an OG logic, which we prove sound w.r.t. the semantics, and a verification condition generator, both supporting involved low-level imperative constructs such as function calls and abrupt-termination. We illustrate our framework on an example that features exceptions, guards and function calls. We aim to then target concurrent operating systems, such as the interruptible eChronos embedded operating system for which we already have a model-level OG proof using Hoare-Parallel.

BibTeX Entry

    author           = {Amani, Sidney and Andronick, June and Bortin, Maksym and Lewis, Corey and Christine, Rizkallah and
                        Tuong, Joseph},
    month            = {dec},
    year             = {2016},
    keywords         = {formal verification, programming languages, imperative code, concurrency, owicki-gries, isabelle/hol},
    title            = {Complx: A Verification Framework for Concurrent Imperative Programs},
    booktitle        = {International Conference on Certified Programs and Proofs},
    pages            = {138-150},
    address          = {Paris, France}