The overall problem addressed in this paper is the long-standing problem of program correct- ness, and in particular programs that describe systems of parallel executing processes. We propose a new method for proving correctness of parallel implementations of high-level transition system specifications. The implementation language underlying the method is based on the model of active (or concurrent) ob- jects. The method defines correctness in terms of a simulation relation between the transition system which specifies the program semantics and the transition system that is described by the correctness specification. The simulation relation itself abstracts from the fine-grained interleaving of parallel processes by exploiting a global confluence property of the particular model of active objects considered in this paper. As a proof-of-concept we apply our method to the correctness of a parallel simulator of multicore memory systems.

doi.org/10.48550/arXiv.2302.04661
Computer Security

de Boer, F., Johnsen, E. B., Pun, V. K., & Tapia Tarifa, L. (2023). Proving correctness of parallel implementations of transition system specifications. doi:10.48550/arXiv.2302.04661