{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T13:20:57Z","timestamp":1743081657997,"version":"3.40.3"},"publisher-location":"Singapore","reference-count":31,"publisher":"Springer Singapore","isbn-type":[{"type":"print","value":"9789811618765"},{"type":"electronic","value":"9789811618772"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-981-16-1877-2_2","type":"book-chapter","created":{"date-parts":[[2021,4,8]],"date-time":"2021-04-08T06:03:53Z","timestamp":1617861833000},"page":"14-32","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Algorithm Design Through the Optimization of Reuse-Based Generation"],"prefix":"10.1007","author":[{"given":"Haipeng","family":"Shi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Haihe","family":"Shi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shenghua","family":"Xu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,4,9]]},"reference":[{"issue":"1","key":"2_CR1","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/602382.602403","volume":"50","author":"T Hoare","year":"2003","unstructured":"Hoare, T.: The verifying compiler: a grand challenge for computing research. J. ACM. 50(1), 63\u201369 (2003)","journal-title":"J. ACM."},{"key":"2_CR2","volume-title":"Algorithmics: The Spirit of Computing","author":"D Harel","year":"2004","unstructured":"Harel, D., Feldman, Y.: Algorithmics: The Spirit of Computing, 3rd edn. Addison-Wesley, Upper Saddle River (2004)","edition":"3"},{"issue":"10","key":"2_CR3","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013585 (1969)","journal-title":"Commun. ACM"},{"key":"2_CR4","volume-title":"A Discipline of Programmin","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programmin. Prentice-Hall Inc, Upper Saddle River (1976)"},{"issue":"1","key":"2_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(77)90053-6","volume":"4","author":"R Milner","year":"1977","unstructured":"Milner, R.: Fully abstract models of typed lambda-calculi. Theor. Comput. Sci. 4(1), 1\u201322 (1977)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE. FOCS, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"2_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-5983-1","volume-title":"The Science of Programming","author":"D Gries","year":"1981","unstructured":"Gries, D.: The Science of Programming. Springer, New York (1981). https:\/\/doi.org\/10.1007\/978-1-4612-5983-1"},{"issue":"1","key":"2_CR8","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1145\/602382.602401","volume":"50","author":"J Gray","year":"2003","unstructured":"Gray, J.: What next? a dozen information-technology research goals. J. ACM. 50(1), 41\u201357 (2003)","journal-title":"J. ACM."},{"issue":"6","key":"2_CR9","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1109\/TSE.2005.69","volume":"31","author":"RW Selby","year":"2005","unstructured":"Selby, R.W.: Enabling reuse-based software development of large-scale systems. IEEE T. Software Eng. 31(6), 495\u2013510 (2005)","journal-title":"IEEE T. Software Eng."},{"key":"2_CR10","unstructured":"Franssen, M.: Cocktail: a Tool for Deriving Correct Programs. Ph.D. diss., Eindhoven University of Technology (2000)"},{"key":"2_CR11","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-540-69149-5_20","volume-title":"Verified Software: Theories, Tools, Experiments","author":"DR Smith","year":"2008","unstructured":"Smith, D.R.: Generating Programs plus Proofs by Refinement. In: Meyer, B., Woodcock, J. (eds.) Verified Software: Theories, Tools, Experiments, pp. 182\u2013188. Springer-Verlag, New York (2008). https:\/\/doi.org\/10.1007\/978-3-540-69149-5_20"},{"issue":"1","key":"2_CR12","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1147\/sj.331.0158","volume":"33","author":"VR Yakhnis","year":"1994","unstructured":"Yakhnis, V.R., Farrell, J.A., Shultz, S.S.: Deriving programs using generic algorithms. IBM Syst. J. 33(1), 158\u2013181 (1994)","journal-title":"IBM Syst. J."},{"issue":"7","key":"2_CR13","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1109\/32.605759","volume":"23","author":"G Novak","year":"1997","unstructured":"Novak, G.: Software reuse by specialization of generic procedures through views. IEEE T. Software Eng. 23(7), 401\u2013417 (1997)","journal-title":"IEEE T. Software Eng."},{"issue":"4","key":"2_CR14","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/s11590-009-0126-9","volume":"3","author":"Y Zheng","year":"2009","unstructured":"Zheng, Y., Xu, C., Xue, J.: A simple greedy algorithm for a class of shuttle transportation problems. Optim. Lett. 3(4), 491\u2013497 (2009)","journal-title":"Optim. Lett."},{"issue":"3","key":"2_CR15","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1080\/10556780902797236","volume":"24","author":"J Gon\u00e7alves","year":"2009","unstructured":"Gon\u00e7alves, J., Storer, R., Gondzio, J.: A family of linear programming algorithms based on an algorithm by von Neumann. Optim. Method. Softw. 24(3), 461\u2013478 (2009)","journal-title":"Optim. Method. Softw."},{"issue":"5","key":"2_CR16","doi-asserted-by":"publisher","first-page":"1081","DOI":"10.1080\/10556788.2012.672571","volume":"28","author":"D Breitenreichera","year":"2013","unstructured":"Breitenreichera, D., Lellmanna, J., Schn\u00f6rra, C.: COAL: a generic modelling and prototyping framework for convex optimization problems of variational image analysis. Optim. Method. Softw. 28(5), 1081\u20131094 (2013)","journal-title":"Optim. Method. Softw."},{"key":"2_CR17","unstructured":"Idate, S., Patil, S.H., Mali, D.J.: Automated code generation using generative programming approach for a mathematical expression. In: Proceedings of the International Conference Systemics, Cybernetics and Informatics, pp. 134\u2013137 (2008)"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Nedunuri, S., Cook, W.R.: Synthesis of fast programs for maximum segment sum problems. In: Proceedings of the 8th International Conference on Generative Programming and Component Engineering, pp. 117\u2013126 (2009)","DOI":"10.1145\/1621607.1621626"},{"key":"2_CR19","unstructured":"Robidoux, R., Xu, H., Xing, L., Zhou, M.: Automated modeling of dynamic reliability block diagrams using colored petri nets. IEEE Trans. Syst. Man Cybern. A Syst. Hum. 40(2), 337\u2013351 (2010)"},{"key":"2_CR20","unstructured":"Bolton, M.L., Siminiceanu, R.I., Bass, E.J.: A systematic approach to model checking human-automation interaction using task-analytic models. IEEE Trans. Syst. Man Cybern. A Syst. Hum. 41(5), 961\u2013976 (2011)"},{"key":"2_CR21","unstructured":"Bolton, M.L., Bass, E.J., Siminiceanu, R.I.: Using formal verification to evaluate human-automation interaction: a review. IEEE Trans. Syst. Man Cybern. Syst. 43(3), 488\u2013503 (2013)"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Liu, Y.A.: Systematic Program Design\u2014 from Clarity to Efficiency. Cambridge University Press, Cambridge (2013)","DOI":"10.1017\/CBO9781139567879"},{"key":"2_CR23","unstructured":"Knuth, D.: The Art of Computer Programming, vol. 3: Sorting and Searching, third ed. Addison-Wesley, Massachusetts (1998)"},{"issue":"1","key":"2_CR24","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1093\/comjnl\/23.1.61","volume":"23","author":"K Clark","year":"1980","unstructured":"Clark, K., Darlington, J.: Algorithm classification through synthesis. Comput. J. 23(1), 61\u201365 (1980)","journal-title":"Comput. J."},{"issue":"4","key":"2_CR25","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/BF02943151","volume":"12","author":"J Xue","year":"1997","unstructured":"Xue, J.: A unified approach for developing efficient algorithmic programs. J. Comput. Sci. Tech-CH. 12(4), 314\u2013329 (1997)","journal-title":"J. Comput. Sci. Tech-CH."},{"key":"2_CR26","first-page":"149","volume":"18","author":"J Xue","year":"1997","unstructured":"Xue, J., Davis, R.: A derivation and proof of Knuth\u2019s binary to decimal program. Software-Conc. Tool 18, 149\u2013156 (1997)","journal-title":"Software-Conc. Tool"},{"issue":"6","key":"2_CR27","doi-asserted-by":"publisher","first-page":"553","DOI":"10.1007\/BF02946498","volume":"13","author":"J Xue","year":"1998","unstructured":"Xue, J.: Formal derivation of graph algorithmic programs using partition-and-recur. J. Comput. Sci. Tech-CH. 13(6), 553\u2013561 (1998)","journal-title":"J. Comput. Sci. Tech-CH."},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"Xue, J., Yang, B., Zuo, Z.: A linear in-situ algorithm for the power of cyclic permutation. In: Proceeding of the s 2nd International Frontiers. Algorithmics, pp. 113\u2013123 (2008)","DOI":"10.1007\/978-3-540-69311-6_14"},{"key":"2_CR29","doi-asserted-by":"publisher","unstructured":"Xue, J., Zheng, Y., Hu, Q., et al.: PAR: a practicable formal method and\u00a0its supporting platform. In: Sun, J., Sun, M. (eds.), ICFEM 2018. LNCS, vol. 11232. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02450-5_5","DOI":"10.1007\/978-3-030-02450-5_5"},{"key":"2_CR30","volume-title":"Categories, Types and Structures: An Introduction to Category Theory for the Working Computer Scientist","author":"A Asperti","year":"1991","unstructured":"Asperti, A., Longo, G.: Categories, Types and Structures: An Introduction to Category Theory for the Working Computer Scientist. MIT Press, Cambridge (1991)"},{"key":"2_CR31","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1017\/S0960129500000050","volume":"1","author":"JA Goguen","year":"1991","unstructured":"Goguen, J.A.: A categorical manifesto. Math. Struct. Comput. Sci. 1, 49\u201367 (1991)","journal-title":"Math. Struct. Comput. Sci."}],"container-title":["Communications in Computer and Information Science","Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-16-1877-2_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,23]],"date-time":"2022-12-23T19:31:54Z","timestamp":1671823914000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-981-16-1877-2_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9789811618765","9789811618772"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-981-16-1877-2_2","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"9 April 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NCTCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"National Conference of Theoretical Computer Science","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nanning","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 November 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 November 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nctcs2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"https:\/\/conf.ccf.org.cn\/TCS2020","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"13","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3-5","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3-5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}