Using Hoare logic in a process algebra setting

DOI10.3233/FI-2021-2026MaRDI QIDQ5164860zbMATH OpenOpenAlexFDO

Authors J. A. Bergstra, C. A. Middelburg

Publication date 15 November 2021

Published in Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1906.04491

zbMATH Keywords

asserted processassignment actiondata parameterized actionguarded commandHoare logicprocess algebra

Mathematics Subject Classification ID

Computer science (68-XX)

Recommendations

• Process algebra with guards: Combining hoare logic with process algebra
• scientific article; zbMATH DE number 4016181
• Process expressions and Hoare's logic: Showing and irreconcilability of context-free recursion with Scott's induction rule
• scientific article; zbMATH DE number 3900131
• The ``Hoare Logic of CSP, and All That

Cites work

• A complete inference system for a class of regular behaviours
• A process calculus with finitary comprehended terms
• A Proof System for Communicating Sequential Processes
• A proof technique for communicating sequential processes
• An axiomatic basis for computer programming
• An axiomatic proof technique for parallel programs
• Communicating sequential processes
• Global renaming operators in concrete process algebra
• scientific article; zbMATH DE number 3930354 (Why is no real title available?)
• scientific article; zbMATH DE number 1049169 (Why is no real title available?)
• scientific article; zbMATH DE number 1113856 (Why is no real title available?)
• scientific article; zbMATH DE number 1142323 (Why is no real title available?)
• scientific article; zbMATH DE number 1555176 (Why is no real title available?)
• scientific article; zbMATH DE number 1368948 (Why is no real title available?)
• Process Algebra
• Process algebra for synchronous communication
• Process algebra with guards: Combining hoare logic with process algebra
• Process algebra with propositional signals
• Process algebra with recursive operations
• Soundness and Completeness of an Axiom System for Program Verification
• Splitting bisimulations and retrospective conditions
• The abstract variable-binding calculus
• Verification of sequential and concurrent programs

Cited in

(4)

• Process algebra with guards: Combining hoare logic with process algebra
• scientific article; zbMATH DE number 4118343 (Why is no real title available?)
• A Logical Viewpoint on Process-algebraic Quotients
• scientific article; zbMATH DE number 1424056 (Why is no real title available?)

This page was built for publication: Using Hoare logic in a process algebra setting

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