Formal verification of concurrent programs with Read-write locks

DOI10.1007/S11704-009-0067-6MaRDI QIDQ351980zbMATH OpenOpenAlexFDO

Authors Ming Fu, Yu Zhang, Yong Li

Publication date 4 July 2013

Published in Frontiers of Computer Science in China (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s11704-009-0067-6

zbMATH Keywords

verificationconcurrent separation logicmutual exclusive locksread-write locks

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• Program verification under weak memory consistency using separation logic
• Fine-grained concurrency with separation logic
• Separation logic and concurrency
• Verification of concurrent systems with VerCors
• A separation logic for refining concurrent objects

Cites work

• A Marriage of Rely/Guarantee and Separation Logic
• A semantics for concurrent separation logic
• A syntactic approach to type soundness
• BI as an assertion language for mutable data structures
• Modular verification of concurrent assembly code with dynamic thread creation and termination
• On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning
• Permission accounting in separation logic
• Resources, concurrency, and local reasoning
• Tentative steps toward a development method for interfering programs
• Verification of safety properties for concurrent assembly code
• Verifying properties of parallel programs

Cited in

(5)

• scientific article; zbMATH DE number 1500569 (Why is no real title available?)
• Reasoning about lock placements
• Verification, Model Checking, and Abstract Interpretation
• On the Complexity of Reader-Writer Locks
• Formal verification of language-based concurrent noninterference

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Formal verification of concurrent programs with Read-write locks

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