摘要
The method for software properties proof in interleaving concurrent environment with communication via shared memory is presented here. It was developed to solve the problem of simultaneous check the required property over the family of programs being run arbitrary times in parallel~- instead of doing separate proofs for each number of program instances being run concurrently. Application of this method to real-world industrial tasks is also mentioned in this work, as well as the extended model with new programs dynamical starting and stopping operations.
摘要译文
本文介绍了通过共享内存进行交换并发环境的软件属性证明方法。它的开发是为了解决同时检查并行运行任意时间的程序族的所需属性的问题 - 而不是为每个并发运行的程序实例数做单独的证明。在这项工作中还提到了这种方法在实际工业任务中的应用，以及新程序动态启动和停止操作的扩展模型。
Taras Panchenko;Sunmade Fabunmi. Quality of Concurrent Shared Memory Programs[C]//2018 11th International Conference on the Quality of Information and Communications Technology (QUATIC), Coimbra, Portugal, 4-7 Sept. 2018, PT: IEEE, 2018: 299 - 300