Citation: | ZHANG Yuzhuo, HONG Chunhua, CAO Yuan, et al., “Safety Mechanism Design and Verification of Safety Computer Parallel Program,” Chinese Journal of Electronics, vol. 27, no. 6, pp. 1163-1169, 2018, doi: 10.1049/cje.2018.02.016 |
X. Xu, Y. Lin and X. Yang, “Protocol-aware process placement for MPI programs”, Chinese Journal of Eletronics, Vol.23, No.4, pp.701-705, 2014.
|
A. Bouajjani and M. Emmi, “Analysis of recursively parallel programs”, ACM Sigplan Notices, Vol.47, No.1, pp.203-214, 2011.
|
T. Tian and D. Gong, “Evolutionary generation approach of test data for multiple paths coverage of message-passing parallel programs”, Chinese Journal of Eletronics, Vol.23, No.2, pp.291-296, 2014.
|
Y. Li, Y. Zhang, Y. Chen, et al., “Formal reasoning about lazySTM programs”, Journal of Computer Science and Technology, Vol.25,No.4, pp.841-852, 2010.
|
M. Sousa and I. Dillig, “Cartesian hoare logic for verifying k-safety properties”, ACM SIGPLAN Notices, Vol.51, No.6, pp.57-69, 2016.
|
Z. Yan, H. Jiang, D. Feng, et al., “SUV: A novel single-update version-management scheme for hardware transactional memory systems”, International Journal of Communication Systems, Vol.27, No.12, pp.4166-4184, 2013.
|
D. Aspinall, L. Beringer, M. Hofmann, et al.,“A program logic for resources”, Theoretical Computer Science, Vol.389, No.3, pp.411-445, 2007.
|
A. Saabas and T. Uustalu, “A compositional natural semantics and Hoare logic for low-level languages”, Theoretical Computer Science, Vol.373, No.1, pp.151-168, 2007.
|
V. Vafeiadis, “Concurrent separation logic and operational semantics”, Electronic Notes in Theoretical Computer Science, Vol.276, No.1, pp.335-351, 2011.
|
F. Besson, T. Jensen and D. Pichardie, “Proof-carrying code from certified abstract interpretation and fixpoint compression”, Theoretical Computer Science, Vol.364, No.3, pp.273-291, 2006.
|
N. Shavit and T. Dan, “Software transactional memory”, Distributed Computing, Vol.10, No.2, pp.99-116, 1997.
|
J. Larus and C. Kozyrakis, “Transactional memory”, Communications of the ACM, Vol.51, No.7, pp.80-88, 2007.
|
H.A. Lopez, E.R.B. Marques, F. Martins, et al., “Protocolbased verification of message-passing parallel programs”, ACM SIGPLAN Notices, Vol.50, No.10, pp.280-298, 2015.
|
M. Fu, Y. Zhang and Y. Li, “Formal reasoning about concurrent assembly code with reentrant locks”, IEEE International Symposium on Theoretical Aspects of Software Engineering, IEEE, Tianjin, China, pp.233-240, 2009.
|
Y. Zhu, L. Zhang, S. Wang, et al., “Verifying parallel low-level programs for multi-core processor”, Acta Electronica Sinica, Vol.37, No.S1, pp.1-6, 2009. (in Chinese)
|