A Sound and Complete Shared-Variable Concurrency Model for Multi-threaded Java Programs

DOI10.1007/978-3-540-72952-5_16MaRDI QIDQ5428915zbMATH OpenOpenAlexFDO

Authors Frank S. de Boer

Publication date 28 November 2007

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-72952-5_16

Mathematics Subject Classification ID

Theory of programming languages (68N15) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• An assertion-based proof system for multithreaded Java
• scientific article; zbMATH DE number 1759614
• A shared-variable concurrency analysis of multi-threaded object-oriented programs
• A tool-supported proof system for multithreaded Java.
• A deductive proof system for multithreaded Java with exceptions

Cites work

• A Proof System for Communicating Sequential Processes
• An axiomatic proof technique for parallel programs
• Formal Justification of a Proof System for Communicating Sequential Processes
• scientific article; zbMATH DE number 192929 (Why is no real title available?)
• scientific article; zbMATH DE number 3569793 (Why is no real title available?)
• scientific article; zbMATH DE number 4001463 (Why is no real title available?)
• Ten Years of Hoare's Logic: A Survey—Part I
• The Java memory model

Cited in

(13)

• A shared-variable concurrency analysis of multi-threaded object-oriented programs
• An assertion-based proof system for multithreaded Java
• scientific article; zbMATH DE number 1670511 (Why is no real title available?)
• Run-time checking multi-threaded Java programs
• How to share concurrent wait-free variables
• A dynamic logic for deductive verification of multi-threaded programs
• scientific article; zbMATH DE number 2087419 (Why is no real title available?)
• Reasoning about recursive processes in shared-variable concurrency
• A compositional operational semantics for Java\(_{\text{MT}}\)
• A deductive proof system for multithreaded Java with exceptions
• A tool-supported proof system for multithreaded Java.
• Inductive proof outlines for monitors in Java.
• Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language

Describes a project that uses

Uses Software

• JML

This page was built for publication: A Sound and Complete Shared-Variable Concurrency Model for Multi-threaded Java Programs

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