论文标题
同时命令程序建模，验证和转换的框架
A Framework for Modelling, Verification and Transformation of Concurrent Imperative Programs
论文作者
论文摘要
该论文给出了一个框架的详细介绍，该框架嵌入了简单键入的高阶逻辑中，并旨在支持声音和结构化推理，内容涉及与命令程序模型的各种属性，并具有交织的计算。作为案例研究，将在论文的过程中审查彼得森相互排斥算法的模型，以说明框架的适用性。
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.
