A complete axiomatic semantics of spawning

DOI10.1007/BF02252958zbMath0731.68076MaRDI QIDQ808281

Sigurd Meldal

Publication date: 1991

Published in: Distributed Computing (Search for Journal in Brave)

zbMATH Keywords

concurrent systems; distributed systems; modularity; partial correctness; non-determinism; Ada tasking; task verification

Mathematics Subject Classification ID

68Q10: Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)

68Q60: Specification and verification (program logics, model checking, etc.)

Related Items

Reasoning about dynamically evolving process structures

Uses Software

• Ada95

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A proof system for concurrent ADA programs
• A proof technique for parallel programs
• A linear-history semantics for languages for distributed programming
• An axiomatic semantics for nested concurrency
• Partial correctness of exits from concurrent structures
• Designing equivalent semantic models for process creation
• A proof technique for communicating sequential processes
• Remarks on 'Program proving: Jumps and functions' by M. Clint and C.A.R. Hoare
• Proof rules for the programming language Euclid
• Program proving: KJumps and functions
• Using message passing for distributed programming: proof rules and disciplines
• A Proof System for Communicating Sequential Processes
• Ten Years of Hoare's Logic: A Survey—Part I
• Soundness and Completeness of an Axiom System for Program Verification
• Communicating sequential processes
• A mathematical approach to nondeterminism in data types
• An axiomatic basis for computer programming