2019-12-02
Axiomatic characterization of trace reachability for concurrent objects
Publication
Publication
Presented at the
International Conference on Integrated Formal Methods (December 2019), Bergen, Norway
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.
| Additional Metadata | |
|---|---|
| , , , | |
| doi.org/10.1007/978-3-030-34968-4_9 | |
| Lecture Notes in Computer Science | |
| International Conference on Integrated Formal Methods | |
| Organisation | Computer Security |
|
de Boer, F., & Hiep, H.-D. (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 |
|
