A Hoare logic for dynamic networks of asynchronously communicating deterministic processes

DOI10.1016/S0304-3975(00)00304-2MaRDI QIDQ5958463zbMATH OpenFDO

Authors Frank S. de Boer

Publication date 3 March 2002

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S0304-3975(00)00304-2

zbMATH Keywords

compositionalitycorrectnessdynamic networksHoare logic

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• scientific article; zbMATH DE number 4201637
• A proof system for asynchronously communicating deterministic processes
• scientific article; zbMATH DE number 3890715
• P-A logic - a compositional proof system for distributed programs
• scientific article; zbMATH DE number 1948157

Cites work

• A logic of object-oriented programs
• scientific article; zbMATH DE number 3650529 (Why is no real title available?)
• scientific article; zbMATH DE number 3821076 (Why is no real title available?)
• scientific article; zbMATH DE number 3707731 (Why is no real title available?)
• scientific article; zbMATH DE number 192929 (Why is no real title available?)
• scientific article; zbMATH DE number 3469994 (Why is no real title available?)
• Reasoning about dynamically evolving process structures
• Ten Years of Hoare's Logic: A Survey—Part I

Cited in

(10)

• A UTP approach for rTiMo
• A system for compositional verification of asynchronous objects
• Observable behavior of dynamic systems: component reasoning for concurrent objects
• scientific article; zbMATH DE number 3890715 (Why is no real title available?)
• scientific article; zbMATH DE number 4070296 (Why is no real title available?)
• Observable behavior of distributed systems: component reasoning for concurrent objects
• A sound and complete reasoning system for asynchronous communication with shared futures
• A proof system for asynchronously communicating deterministic processes
• P-A logic - a compositional proof system for distributed programs
• Compositional reasoning about active objects with shared futures

Describes a project that uses

Uses Software

• Smalltalk

This page was built for publication: A Hoare logic for dynamic networks of asynchronously communicating deterministic processes

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