In concurrent object models, objects encapsulate local state, schedule local processes, interact via asynchronous method calls, and methods of different objects are executed concurrently. In this paper, we introduce a compositional trace semantics for concurrent objects and provide an axiomatic characterization of the general properties of reachable traces, that is, traces that can be generated by a concurrent object program. The main result of this paper is a soundness and completeness proof of the axiomatic characterization.
CITATION STYLE
de Boer, F. S., & Hiep, H. D. A. (2019). Axiomatic Characterization of Trace Reachability for Concurrent Objects. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11918 LNCS, pp. 157–174). Springer. https://doi.org/10.1007/978-3-030-34968-4_9
Mendeley helps you to discover research relevant for your work.