PVS Embedding of cCSP Semantic Models and Their Relationship

DOI10.1016/j.entcs.2009.08.020zbMath1335.68129OpenAlexW2109375135WikidataQ59625926 ScholiaQ59625926MaRDI QIDQ5178979

Michael J. Butler, Shamim H. Ripon

Publication date: 18 March 2015

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2009.08.020

zbMATH Keywords

embeddinginductionsemantic modelsPVScompensating CSP

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (1)

Failure-divergence semantics and refinement of long running transactions

Uses Software

• Coq
• Isabelle
• ML
• PVS
• HOL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Isabelle. A generic theorem prover
• A structural approach to operational semantics
• Verifying security protocols with PVS: widening the rank function approach
• Process Algebra

This page was built for publication: PVS Embedding of cCSP Semantic Models and Their Relationship