{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T06:38:49Z","timestamp":1757313529496,"version":"3.41.0"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2016,10,20]],"date-time":"2016-10-20T00:00:00Z","timestamp":1476921600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Nature Science Foundation of China","doi-asserted-by":"crossref","award":["61462041","61462039"],"award-info":[{"award-number":["61462041","61462039"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001809","name":"National Nature Science Foundation of China","doi-asserted-by":"crossref","award":["61472167"],"award-info":[{"award-number":["61472167"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"National Natural Science Foundation of Jiangxi Province","award":["20142BAB217023"],"award-info":[{"award-number":["20142BAB217023"]}]},{"name":"Science and Technology Research Project of Jiangxi Province Educational Department","award":["GJJ14268"],"award-info":[{"award-number":["GJJ14268"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Cluster Comput"],"published-print":{"date-parts":[[2016,12]]},"DOI":"10.1007\/s10586-016-0663-9","type":"journal-article","created":{"date-parts":[[2016,10,20]],"date-time":"2016-10-20T02:23:07Z","timestamp":1476930187000},"page":"2145-2156","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Unified formal derivation and automatic verification of three binary-tree traversal non-recursive algorithms"],"prefix":"10.1007","volume":"19","author":[{"given":"Zhen","family":"You","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jinyun","family":"Xue","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhengkang","family":"Zuo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,10,20]]},"reference":[{"key":"663_CR1","doi-asserted-by":"crossref","unstructured":"Wu, C., Li, G., Huang, C. et al.: Adaptive index deletion in XML document based on tree traversal order. In: 2nd International Conference on Biomedical Engineering and Informatics BMEI\u201909, IEEE, pp. 1\u20134 (2009)","DOI":"10.1109\/BMEI.2009.5304820"},{"issue":"12","key":"663_CR2","doi-asserted-by":"crossref","first-page":"6923","DOI":"10.1016\/j.jde.2015.08.017","volume":"259","author":"K Ammari","year":"2015","unstructured":"Ammari, K., Mercier, D., R\u00e9gnier, V.: Spectral analysis of the Schr\u00f6dinger operator on binary tree-shaped networks and applications. J. Differ. Equ. 259(12), 6923\u20136959 (2015)","journal-title":"J. Differ. Equ."},{"key":"663_CR3","doi-asserted-by":"crossref","unstructured":"Poornima, A.S., Amberker, B.B.: Binary tree based cluster key management scheme for heterogeneous sensor networks. In: 2008 16th IEEE International Conference on Networks. pp. 1\u20136 (2008)","DOI":"10.1109\/ICON.2008.4772567"},{"issue":"4","key":"663_CR4","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1109\/TC.1981.1675772","volume":"100","author":"E Horowitz","year":"1981","unstructured":"Horowitz, E., Zorat, A.: The binary tree as an interconnection network: applications to multiprocessor systems and VLSI. IEEE Trans. Comput. 100(4), 247\u2013253 (1981)","journal-title":"IEEE Trans. Comput."},{"issue":"2\u20133","key":"663_CR5","first-page":"127","volume":"8","author":"Q Dai","year":"2005","unstructured":"Dai, Q., Wu, J.: Computation of minimal uniform transmission range in ad hoc wireless networks. Clust. Comput. J. Netw. Softw. Tools Appl. 8(2\u20133), 127\u2013133 (2005)","journal-title":"Clust. Comput. J. Netw. Softw. Tools Appl."},{"issue":"2","key":"663_CR6","first-page":"199","volume":"13","author":"K Xu","year":"2010","unstructured":"Xu, K., Song, M., Song, J.: An improved P2P lookup protocol model. Clust. Comput. J. Netw. Softw. Tools Appl. 13(2), 199\u2013211 (2010)","journal-title":"Clust. Comput. J. Netw. Softw. Tools Appl."},{"key":"663_CR7","doi-asserted-by":"crossref","unstructured":"Ruijun, Z., Bichao, G.: Application of RSA encryption algorithm based on binary tree in truck scale Weighing system. In: 2011 International Conference on Internet Technology and Applications (iTAP), IEEE, pp. 1\u20134 (2011)","DOI":"10.1109\/ITAP.2011.6006183"},{"key":"663_CR8","doi-asserted-by":"crossref","unstructured":"Lu, Y., Li, J.: Constructing forward-secure identity-based encryption from identity-based binary tree encryption. In: 2012 International Symposium on Information Science and Engineering (ISISE), IEEE, pp. 199\u2013202 (2012)","DOI":"10.1109\/ISISE.2012.50"},{"issue":"2","key":"663_CR9","doi-asserted-by":"crossref","first-page":"133","DOI":"10.14257\/ijgdc.2015.8.2.13","volume":"8","author":"S Mao","year":"2015","unstructured":"Mao, S., Zang, H., Ni, B.: Research on semantic web service composition based on binary tree. Int. J. Grid Distrib. Comput. 8(2), 133\u2013142 (2015)","journal-title":"Int. J. Grid Distrib. Comput."},{"key":"663_CR10","doi-asserted-by":"crossref","unstructured":"Nomura, A., Matsuba, H., Ishikawa Y.: Network performance model for TCP\/IP based cluster computing. In: IEEE International Conference on Cluster Computing, pp. 194\u2013203 (2007)","DOI":"10.1109\/CLUSTR.2007.4629232"},{"key":"663_CR11","unstructured":"Jones, T.O.: Fifth Gen White Paper: The Fifth Gen Bianry Tree Cluster Computer (BTC-100X). http:\/\/www.fifthgen.com\/pdf\/Overview120809.pdf . Accessed July 2016"},{"key":"663_CR12","series-title":"LNCS","volume-title":"Isabelle\/HOL A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2001","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, New York (2001)"},{"key":"663_CR13","doi-asserted-by":"crossref","unstructured":"Blanchette, J. C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle\/HOL. In: Frontiers of Combining Systems. Springer, Berlin, pp. 12\u201327 (2011)","DOI":"10.1007\/978-3-642-24364-6_2"},{"key":"663_CR14","unstructured":"Nipkow, T.: Programming and Proving in Isabelle\/HOL. http:\/\/isabelle.in.tum.de\/dist\/Isabelle2016\/doc\/prog-prove.pdf . Accessed July 2016"},{"key":"663_CR15","unstructured":"Nipkow, T., Paulson, L. C., Wenzel, M.: A Proof Assistant for Higher-Order Logic. Version of February 17, 2016. http:\/\/isabelle.in.tum.de\/doc\/tutorial.pdf . Accessed July 2016"},{"key":"663_CR16","doi-asserted-by":"crossref","unstructured":"Xue, J.: A unified approach for developing efficient algorithm of programs. J. Comput. Sci. Technol. 12(4), 314\u2013329 (1997)","DOI":"10.1007\/BF02943151"},{"key":"663_CR17","unstructured":"Jinyun, X.: PAR method and its supporting platform. In: Proceedings of the 1st Asian working Conference on Verified Software (AWCVS 2006), pp. 29\u201331 (2006)"},{"issue":"1","key":"663_CR18","first-page":"77","volume":"40","author":"F Tian","year":"2016","unstructured":"Tian, F., Shi, H., Zuo, Z., Wang, C., Xue, J.: The java-based novel implementation for an abstract generic mechanism computer engineering and applications. J. Jiangxi Norm. Univ. (Nat. Sci. Ed.) 40(1), 77\u201382 (2016). (in Chinese)","journal-title":"J. Jiangxi Norm. Univ. (Nat. Sci. Ed.)"},{"key":"663_CR19","unstructured":"Xue, J., Davis, R: A simple program whose derivation and proof is also. In: Proceedings of the International Conference on Formal Engineering Methods, ICFEM, pp. 132\u2013139 (1997)"},{"key":"663_CR20","unstructured":"Gries, D., Xue J.Y.: The Hopcroft\u2013tarjan Planarity Algorithm, Presentations and Improvements. Technical Report 88\u2013906, Computer Science Department, Cornell University (1988)"},{"key":"663_CR21","unstructured":"Wuping, X.: Implementation of Hopcroft\u2013Tarjan Planarity Testing Algorithm in Apla Language. Technical Report of Jiangxi Normal University (in Chinese) (2009)"},{"key":"663_CR22","doi-asserted-by":"crossref","unstructured":"Xue, J.Y., Yang, B., Zuo Z.K.: A Linear in-situ algorithm for the power of cyclic permutation. In: Proceedings of the 2nd Int\u2019l Frontiers of Algorithmics Workshop (FAW 2008). LNCS 5059, Heidelberg: Springer, pp. 113\u2013123 (2008)","DOI":"10.1007\/978-3-540-69311-6_14"},{"issue":"4","key":"663_CR23","first-page":"378","volume":"38","author":"Y Huanglei","year":"2014","unstructured":"Huanglei, Y., Jinyun, X.: The research on methods of developing a class of loop invariants of single-variable-assignment type. J. Jiangxi Norm. Univ. (Nat. Sci. Ed.) 38(4), 378\u2013382 (2014)","journal-title":"J. Jiangxi Norm. Univ. (Nat. Sci. Ed.)"},{"key":"663_CR24","unstructured":"Yang, B.: Implementation of Bank Management System in Apla Language. Technical Report of Jiangxi Normal University, (in Chinese) (2008)"},{"key":"663_CR25","unstructured":"Wu G.: The Application and Research of PAR Platform in Software Outsourcing Services [MS. Thesis]. Nanchang: Jiangxi Normal University (in Chinese with English abstract) (2013)"},{"issue":"2","key":"663_CR26","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF02939477","volume":"8","author":"X Jinyun","year":"1993","unstructured":"Jinyun, X.: Two new strategies for developing loop invariants and their applications. J. Comput. Sci. Technol. 8(2), 147\u2013154 (1993). (in Chinese)","journal-title":"J. Comput. Sci. Technol."},{"key":"663_CR27","unstructured":"Jinyun, X.: PAR method: abstract programming language apla. Technical report. Key Laboratory of high performance computing technology, Jiangxi Normal University (in Chinese) (2001)"},{"key":"663_CR28","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"663_CR29","volume-title":"Predicate Calculus and Program Semantics","author":"EW Dijkstra","year":"1989","unstructured":"Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, New York (1989)"},{"key":"663_CR30","first-page":"85","volume":"10","author":"Y Zhen","year":"2009","unstructured":"Zhen, Y., Jinyun, X.: Formal verification of algorithm program based on Isabelle theorem prover. Comput. Eng. Sci. 10, 85\u201389 (2009). (in Chinese)","journal-title":"Comput. Eng. Sci."},{"key":"663_CR31","first-page":"119","volume":"03","author":"Z Zuo","year":"2010","unstructured":"Zuo, Z., You, Z.: Derivation and formal proof of the binary tree non-recursive algorithm for the post-order traversal. Comput. Eng. Sci. 03, 119\u2013123 (2010). (in Chinese)","journal-title":"Comput. Eng. Sci."},{"issue":"10","key":"663_CR32","first-page":"25","volume":"43","author":"N Arora","year":"2012","unstructured":"Arora, N., Kumar Tamta, V., Kumar, S.: Modified non-recursive algorithm for reconstructing a binary tree. Int. J. Comput. Appl. 43(10), 25\u201328 (2012)","journal-title":"Int. J. Comput. Appl."},{"key":"663_CR33","first-page":"032","volume":"4","author":"LUO Shuai","year":"2008","unstructured":"Shuai, L.U.O.: The analysis and realization of traversing binary tree with non-recursive algorithm. Comput. Knowl. Technol. 4, 032 (2008)","journal-title":"Comput. Knowl. Technol."},{"key":"663_CR34","doi-asserted-by":"crossref","unstructured":"Das V.V.: A new non-recursive algorithm for reconstructing a binary tree from its traversals. In: 2010 International Conference on Advances in Recent Technologies in Communication and Computing (ARTCom), IEEE, pp. 261\u2013263 (2010)","DOI":"10.1109\/ARTCom.2010.88"},{"key":"663_CR35","first-page":"222","volume":"63","author":"M Wang","year":"2011","unstructured":"Wang, M.: Non-recursive simulation on the recursive algorithm of binary tree reverting to its corresponding forest in intelligent materials. Appl. Mech. Mater. 63, 222\u2013225 (2011)","journal-title":"Appl. Mech. Mater."},{"key":"663_CR36","first-page":"261","volume-title":"Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm. Static Analysis.","author":"A Loginov","year":"2006","unstructured":"Loginov, A., Reps, T., Sagiv, M.: Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm. Static Analysis., pp. 261\u2013279. Springer, Berlin (2006)"}],"container-title":["Cluster Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10586-016-0663-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10586-016-0663-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10586-016-0663-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T18:01:43Z","timestamp":1749664903000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10586-016-0663-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,10,20]]},"references-count":36,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,12]]}},"alternative-id":["663"],"URL":"https:\/\/doi.org\/10.1007\/s10586-016-0663-9","relation":{},"ISSN":["1386-7857","1573-7543"],"issn-type":[{"type":"print","value":"1386-7857"},{"type":"electronic","value":"1573-7543"}],"subject":[],"published":{"date-parts":[[2016,10,20]]}}}