Mechanization of LAGC Semantics in Isabelle

TL;DR

This paper formalizes the Locally Abstract, Globally Concrete (LAGC) semantics in Isabelle/HOL, enabling rigorous reasoning and proof automation for concurrent program semantics based on prior theoretical work.

Contribution

It provides a formal, modular Isabelle/HOL implementation of LAGC semantics, including proofs of key properties and code-generation for trace computation.

Findings

Formalization of LAGC semantics in Isabelle/HOL

Proofs of advanced properties of LAGC semantics

Efficient code-generation for program trace computation

Abstract

Formal programming language semantics are imperative when trying to verify properties of programs in an automated manner. Using a new approach, Din et al. strengthen the ability of reasoning about concurrent programs by proposing a modular trace semantics, which can flexibly adapt to the most prominent imperative programming language paradigms. These semantics decouple the evaluation in the local environments from the evaluation in the global environment by generating abstract, symbolic traces for the individual, local systems. The traces are then composed and concretized, resulting in global traces for the global system. Hence, these semantics are called Locally Abstract, Globally Concrete (LAGC). In this work, we present a formalization of the LAGC semantics in the popular theorem proving environment Isabelle/HOL. The given model is based on the prior work on the theory of LAGC semantics by Din et al. and includes formalizations of the basic theorems, the LAGC semantics for the While Language (WL), as well as the LAGC semantics for an extended version of the While Language (WLEXT). We furthermore use our Isabelle model in order to provide formal proofs for several advanced properties of the LAGC semantics, which have not been analyzed in the original paper. Whilst the main goal of the work was to formalize the LAGC semantics in a mathematically rigorous manner, we also achieve a high level of proof automatization and manage to contribute an efficient code-generation for the computation of program traces. As the formalization of the semantics is highly modular, the given theories could in the future be extended with even more sophisticated programming language paradigms.