A UTP semantics for communicating processes with shared variables and its formal encoding in PVS
type: Item
instance of: scholarly article
title: A UTP semantics for communicating processes with shared variables and its formal encoding in PVS
zbMATH Open document ID: 1398.68373
author: Ling Shi
author: Yongxin Zhao
author: Yang Liu
author: Jun Sun
author: Shengchao Qin
author: Jin-Song Dong
published in: Formal Aspects of Computing
publication date: 2018-10-23T00:00:00Z
full work available at URL: http://hdl.handle.net/10072/381740
Mathematics Subject Classification ID: 68Q85
Mathematics Subject Classification ID: 68Q55
zbMATH DE Number: 6962867
zbMATH Keywords: UTP
zbMATH Keywords: denotational semantics
zbMATH Keywords: shared variables
zbMATH Keywords: encoding
describes a project that uses: Isabelle
describes a project that uses: ProofPower
describes a project that uses: PAT
describes a project that uses: PTSC
describes a project that uses: Circus
describes a project that uses: TCOZ
describes a project that uses: Coq
describes a project that uses: CSP-prover
describes a project that uses: ML
describes a project that uses: PVS
describes a project that uses: HOL
MaRDI profile type: Publication
OpenAlex ID: W2799615765
cites work: Full abstraction for a shared-variable parallel language
cites work: CSP with Hierarchical State
cites work: Q5563096
cites work: Unifying Theories in Isabelle/HOL
cites work: Unifying Theories of Programming in Isabelle
cites work: Q5287513
cites work: Laws of programming
cites work: Q3777424
cites work: Tools and Algorithms for the Construction and Analysis of Systems
cites work: Proof Principles of CSP – CSP-Prover in Practice
cites work: Deep semantic links of TCSP and Object-Z: TCOZ approach.
cites work: Q3992568
cites work: Unifying Theories in ProofPower-Z
cites work: A UTP semantics for \textsf{Circus}
cites work: Isabelle. A generic theorem prover
cites work: The Stable Revivals Model in CSP-Prover
cites work: CSP theorems for communicating B machines
cites work: Q4472182
cites work: Q3141916
cites work: Q4787253
cites work: Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language
Wikidata QID: Q129925329
DOI: 10.1007/S00165-018-0453-7
description: scientific article; zbMATH DE number 6962867