Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP article: Complx


view this post on Zulip Email Gateway (Aug 22 2022 at 14:30):

From: Tobias Nipkow <nipkow@in.tum.de>
COMPLX: A Verification Framework for Concurrent Imperative Programs
Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah
and Joseph Tuong

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 Complx language, extending the syntax and semantics of Simpl 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.

https://www.isa-afp.org/entries/Complx.shtml

Enjoy!
smime.p7s


Last updated: Mar 29 2024 at 12:28 UTC