Formal verification of concurrent programs with Read-write locks

DOI10.1007/s11704-009-0067-6zbMath1267.68141OpenAlexW2021598894MaRDI QIDQ351980

Yong Li, Yu Zhang, Ming Fu

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

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

Uses Software

• Coq

Cites Work

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

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