A Formal System for Specification Analysis of Concurrent Programs

Ken Hirose; Makoto Takahashi

doi:10.2977/prims/1195182015

JournalsprimsVol. 19, No. 3pp. 911–926

A Formal System for Specification Analysis of Concurrent Programs

Ken Hirose
Waseda University, Tokyo, Japan
Makoto Takahashi
Waseda University, Tokyo, Japan

Download PDF

Abstract

A formal system $FL_{m, n}$ is proposed to analyze the specification of concurrent programs. The soundness theorem for $FL_{m, n}$ is also proved.

Cite this article

Ken Hirose, Makoto Takahashi, A Formal System for Specification Analysis of Concurrent Programs. Publ. Res. Inst. Math. Sci. 19 (1983), no. 3, pp. 911–926

DOI 10.2977/PRIMS/1195182015