A formal system for specification analysis of concurrent programs

DOI10.2977/PRIMS/1195182015MaRDI QIDQ792086zbMATH OpenOpenAlexFDO

Authors Ken Hirose, Makoto Takahashi

Publication date 1983

Published in Publications of the Research Institute for Mathematical Sciences, Kyoto University (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2977/prims/1195182015

zbMATH Keywords

forcing logicspecification of concurrent programstwo-sorted language

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Review text

A formal system, which consists of two-sorted language and twelve deduction rules, based on the forcing logic (FL) formulas, is proposed to analyze the specification of concurrent programs. The system may be easily extended to a formal system containing the ordinary predicate logic formulas only (although this extension is not described in the paper).

Recommendations

• Formal Specification of Concurrent Systems: A Structured Approach
• Specification and verification of concurrent programs through refinements
• A functional programming approach to the specification and verification of concurrent systems
• scientific article; zbMATH DE number 107452
• Specification and verification of concurrent systems by causality and realizability

Cited in

(9)

• Language-oriented formal analysis: a case study on protocols and distributed systems
• scientific article; zbMATH DE number 3874577 (Why is no real title available?)
• Specifying and Analysing SOC Applications with COWS
• scientific article; zbMATH DE number 1487742 (Why is no real title available?)
• scientific article; zbMATH DE number 749804 (Why is no real title available?)
• scientific article; zbMATH DE number 911851 (Why is no real title available?)
• scientific article; zbMATH DE number 1390334 (Why is no real title available?)
• scientific article; zbMATH DE number 5262134 (Why is no real title available?)
• Distributed Computing

This page was built for publication: A formal system for specification analysis of concurrent programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q792086)