A calculus of atomic actions

DOI10.1145/1480881.1480885zbMATH Open1315.68087OpenAlexW2155487709MaRDI QIDQ5261501FDOQ5261501

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

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

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)

Cited In (23)

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

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)