Partial correctness of exits from concurrent structures

DOI10.1007/BF01933709MaRDI QIDQ1080654zbMATH OpenOpenAlexFDO

Authors Sigurd Meldal

Publication date 1986

Published in BIT (Search for Journal in Brave)

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

zbMATH Keywords

communicating sequential processesCSPdata flow systemparallel commandpre- and postconditions

Mathematics Subject Classification ID

Theory of operating systems (68N25) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

A rudimentary exit-mechanism from the parallel command of the language fragment CSP is introduced. A method for embedding invariants in a standard partial correctness system with pre- and postconditions is presented. Proof rules for exits from concurrent systems are introduced, and a simple data flow system is verified.

Recommendations

• scientific article; zbMATH DE number 3878340
• scientific article; zbMATH DE number 3963180
• scientific article; zbMATH DE number 3903944
• A proof system for concurrent ADA programs
• scientific article; zbMATH DE number 3907747

Cites work

• Ada exception handling: an axiomatic approach
• An axiomatic semantics for nested concurrency
• Communicating sequential processes
• Partial correctness of exits from concurrent structures
• Soundness and Completeness of an Axiom System for Program Verification
• Ten Years of Hoare's Logic: A Survey—Part I

Cited in

(3)

• Partial correctness of exits from concurrent structures
• Axiomatic treatment of processes with shared variables revisited
• A complete axiomatic semantics of spawning

Describes a project that uses

Uses Software

• Ada95

This page was built for publication: Partial correctness of exits from concurrent structures

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