Process algebra with guards: Combining hoare logic with process algebra

DOI10.1007/BF01221097MaRDI QIDQ1329197zbMATH OpenOpenAlexFDO

Authors Jan Friso Groote, Alban Ponse

Publication date 29 June 1994

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf01221097

zbMATH Keywords

bisimulationHoare logicoperational semanticsprocess algebra with guards

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Using Hoare logic in a process algebra setting
• Process expressions and Hoare's logic: Showing and irreconcilability of context-free recursion with Scott's induction rule
• Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS
• Process algebra with four-valued logic
• scientific article; zbMATH DE number 3900131

Cites work

• A generalization of Owicki-Gries's Hoare logic for a concurrent while language
• A proof system for communicating processes with value-passing
• Algèbre de processus et synchronisation
• An axiomatic basis for computer programming
• An axiomatic proof technique for parallel programs
• Equational bases of boolean algebras
• Global renaming operators in concrete process algebra
• scientific article; zbMATH DE number 3928334 (Why is no real title available?)
• scientific article; zbMATH DE number 3958712 (Why is no real title available?)
• scientific article; zbMATH DE number 3967883 (Why is no real title available?)
• scientific article; zbMATH DE number 4037177 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 3664335 (Why is no real title available?)
• scientific article; zbMATH DE number 3707731 (Why is no real title available?)
• scientific article; zbMATH DE number 3716792 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 3550181 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 1028829 (Why is no real title available?)
• scientific article; zbMATH DE number 3894457 (Why is no real title available?)
• Laws of programming
• Process Algebra
• Process algebra for synchronous communication
• Process expressions and Hoare's logic: Showing and irreconcilability of context-free recursion with Scott's induction rule
• Real time process algebra
• Ten years of Hoare's logic: A survey. II: Nondeterminism
• Ten Years of Hoare's Logic: A Survey—Part I
• The linear time -- branching time spectrum. I: The semantics of concrete, sequential processes.

Cited in

(14)

• Process expressions and Hoare's logic: Showing and irreconcilability of context-free recursion with Scott's induction rule
• On sequential composition, action prefixes and process prefix
• The algebra of communicating processes with empty process
• Process algebra with propositional signals
• Process algebra for hybrid systems
• Notions of bisimulation and congruence formats for SOS with data
• Compositional Abstraction in Real-Time Model Checking
• scientific article; zbMATH DE number 4060687 (Why is no real title available?)
• Process algebra with four-valued logic
• A ground-complete axiomatization of stateless bisimilarity over Linda
• scientific article; zbMATH DE number 7080198 (Why is no real title available?)
• Using Hoare logic in a process algebra setting
• Sequential value passing yields a Kleene theorem for processes
• Revisiting sequential composition in process calculi

This page was built for publication: Process algebra with guards: Combining hoare logic with process algebra

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