A generalization of Owicki-Gries's Hoare logic for a concurrent while language

DOI10.1016/0304-3975(88)90033-3zbMath0653.03017OpenAlexW2071748540MaRDI QIDQ1107518

Colin Stirling

Publication date: 1988

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

Full work available at URL: https://doi.org/10.1016/0304-3975(88)90033-3

zbMATH Keywords

parallel programsHoare logicprogram verificationconcurrent while languageparallal language semantics

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Process algebra with guards: Combining hoare logic with process algebra, Hoare Logic for Disjunctive Information Flow, Parallel composition of assumption-commitment specifications: A unifying approach for shared variable and distributed message passing concurrency, The Rely-Guarantee method for verifying shared variable concurrent programs, On Rely-Guarantee Reasoning, Proving properties of dynamic process networks, Modular verification for shared-variable concurrent programs, Interpreting one concurrent calculus in another, Axiomatic treatment of processes with shared variables revisited, Compositional analysis of C/C++ programs with veriSoft, An explanatory presentation of composition rules for assumption- commitment specifications

Cites Work

• The Hoare logic of concurrent programs
• A proof technique for parallel programs
• Recursive assertions and parallel programs
• An axiomatic proof technique for parallel programs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item