Barriers in concurrent separation logic: now with tool support!

DOI10.2168/LMCS-8(2:2)2012MaRDI QIDQ2887058zbMATH OpenFDO

Authors Aquinas Hobor, Cristian Gherghina

Publication date 16 May 2012

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2168/LMCS-8(2:2)2012

zbMATH Keywords

concurrencyconcurrent separation logicverification tools

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Barriers in Concurrent Separation Logic
• Separation logic and concurrency
• CONCUR 2004 - Concurrency Theory
• Revisiting concurrent separation logic
• A semantics for concurrent separation logic

Cited in

(4)

• On automation in the verification of software barriers: experience report
• Barriers in Concurrent Separation Logic
• Expressing the behavior of three very different concurrent systems by using natural extensions of separation logic
• Verification of concurrent systems with VerCors

Describes a project that uses

Uses Software

• Coq
• VeriSmall
• pthreads
• Mechanized Semantic Library

This page was built for publication: Barriers in concurrent separation logic: now with tool support!

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