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.

翻译：本文详细阐述了一个嵌入简单类型高阶逻辑的框架，旨在支持对具有交错计算的命令式程序模型的各种属性进行可靠且结构化的推理。作为案例研究，本文将以彼得森互斥算法模型为例，深入剖析该框架的适用性。