Email Gateway (Aug 22 2022 at 14:30): 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: Nov 21 2024 at 12:39 UTC