A Framework for Modelling, Verification and Transformation of Concurrent Imperative Programs

TL;DR

This paper presents a framework embedded in higher-order logic for modeling, verifying, and transforming concurrent imperative programs, demonstrated through a case study on Peterson's mutual exclusion algorithm.

Contribution

It introduces a structured framework for reasoning about concurrent imperative programs within a higher-order logic setting, including verification and transformation capabilities.

Findings

Framework supports sound reasoning about concurrent programs

Successful modeling and verification of Peterson's algorithm

Framework demonstrates applicability to real-world concurrent algorithms

Abstract

The paper gives a detailed presentation of a framework, embedded into the simply typed higher-order logic and aimed at the support of sound and structured reasoning about various properties of models of imperative programs with interleaved computations. As a case study, a model of the Peterson's mutual exclusion algorithm will be scrutinised in the course of the paper illustrating applicability of the framework.