Formal verification of concurrent programs with Read-write locks

DOI10.1007/S11704-009-0067-6zbMATH Open1267.68141OpenAlexW2021598894MaRDI QIDQ351980FDOQ351980

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

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

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)

Cites Work

• BI as an assertion language for mutable data structures
• A semantics for concurrent separation logic
• Verifying properties of parallel programs
• Permission accounting in separation logic
• Resources, concurrency, and local reasoning
• Tentative steps toward a development method for interfering programs
• 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
• Verification of safety properties for concurrent assembly code
• On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning

Cited In (5)

• Reasoning about lock placements
• Formal verification of language-based concurrent noninterference
• Title not available (Why is that?)
• Verification, Model Checking, and Abstract Interpretation
• On the Complexity of Reader-Writer Locks

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)