Barriers in Concurrent Separation Logic

DOI10.1007/978-3-642-19718-5_15zbMath1326.68096arXiv1203.6412OpenAlexW2153880165MaRDI QIDQ3000585

Aquinas Hobor, Cristian Gherghina

Publication date: 19 May 2011

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1203.6412

Mathematics Subject Classification ID

Related Items (2)

Verification of Concurrent Systems with VerCors ⋮ On automation in the verification of software barriers: experience report

Uses Software

• Coq
• pthreads
• Mechanized Semantic Library

Cites Work

• Resources, concurrency, and local reasoning
• Local Reasoning for Storable Locks and Threads
• Separation Logic for Small-Step cminor
• Interprocedural Shape Analysis with Separated Heap Abstractions
• Concurrent Separation Logic for Pipelined Parallelization
• A theory of indirection via approximation
• Permission accounting in separation logic
• CONCUR 2004 - Concurrency Theory
• Expressive modular fine-grained concurrency specification
• Oracle Semantics for Concurrent Separation Logic

This page was built for publication: Barriers in Concurrent Separation Logic