Natural reductions for concurrent programs admit a sound-and-complete polynomial-time soundness check without synchronization but are coNP-hard under locking.
In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation
3 Pith papers cite this work. Polarity classification is still indexing.
3
Pith papers citing it
citation-role summary
baseline 1
citation-polarity summary
years
2026 3roles
baseline 1polarities
baseline 1representative citing papers
VerCors-relaxed encodes SLR logic to automatically verify weak memory concurrent programs with realistic performance on literature examples.
Multiple-choice queries synthesized from Hoare triples enable more reliable identification of intended programs than labeled-example supervision in active learning for program disambiguation.
citing papers explorer
-
On the Complexity of Checking Soundness of Natural Reductions (Extended Version)
Natural reductions for concurrent programs admit a sound-and-complete polynomial-time soundness check without synchronization but are coNP-hard under locking.
-
Deductive Verification of Weak Memory Programs with View-based Protocols (extended version)
VerCors-relaxed encodes SLR logic to automatically verify weak memory concurrent programs with realistic performance on literature examples.
-
Choose, Don't Label: Multiple-Choice Query Synthesis for Program Disambiguation
Multiple-choice queries synthesized from Hoare triples enable more reliable identification of intended programs than labeled-example supervision in active learning for program disambiguation.