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.

Concurrency, Compositionality, Completeness, Program synthesis
dx.doi.org/10.1007/978-3-030-34968-4_9
Lecture Notes in Computer Science
International Conference on Integrated Formal Methods
Computer Security

de Boer, F.S, & Hiep, H.A. (2019). Axiomatic characterization of trace reachability for concurrent objects. In Proceedings of the 15th International Conference on integrated Formal Methods (pp. 157–174). doi:10.1007/978-3-030-34968-4_9