A calculus of atomic actions

DOI10.1145/1480881.1480885MaRDI QIDQ5261501zbMATHOpenAlexFDO

Authors Tayfun Elmas, Serdar Tasiran, Shaz Qadeer

Publication date 3 July 2015

Published in Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1480881.1480885

zbMATH Keywords

abstractionreductionatomicityconcurrent programs

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• A criterion for atomicity
• The Rely-Guarantee method for verifying shared variable concurrent programs
• scientific article; zbMATH DE number 3956417
• scientific article; zbMATH DE number 3902009
• Modular verification for shared-variable concurrent programs

Cited in

(23)

• Model checking concurrent programs
• scientific article; zbMATH DE number 1612485 (Why is no real title available?)
• On automation in the verification of software barriers: experience report
• Flashix: modular verification of a concurrent and crash-safe flash file system
• scientific article; zbMATH DE number 4121471 (Why is no real title available?)
• Starling: lightweight concurrency verification with views
• Verifying a concurrent garbage collector using a rely-guarantee methodology
• A criterion for atomicity
• Verifying a concurrent garbage collector with a rely-guarantee methodology
• A mechanized proof environment for the convenient computations proof method
• scientific article; zbMATH DE number 7136664 (Why is no real title available?)
• Distributed Computing
• Layered concurrent programs
• Multithreaded testing of program interfaces
• Commutativity for concurrent program termination proofs
• A Coq library for verification of concurrent programs
• Dynamic reductions for model checking concurrent software
• Synchronizing the asynchronous
• An assertional proof for a construction of an atomic variable
• Model Checking Software
• Verifying the correctness of distributed systems via mergeable parallelism
• A mechanized refinement proof of the Chase-Lev deque using a proof system
• Resource protection using atomics. Patterns and verification

This page was built for publication: A calculus of atomic actions

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