{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T17:33:43Z","timestamp":1743010423261,"version":"3.40.3"},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030046170"},{"type":"electronic","value":"9783030046187"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","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":[[2018]]},"DOI":"10.1007\/978-3-030-04618-7_7","type":"book-chapter","created":{"date-parts":[[2018,11,16]],"date-time":"2018-11-16T20:47:58Z","timestamp":1542401278000},"page":"74-87","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Novel Approach to Verifying Context Free Properties of Programs"],"prefix":"10.1007","author":[{"given":"Nan","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cong","family":"Tian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hongwei","family":"Du","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,11,17]]},"reference":[{"key":"7_CR1","unstructured":"IEC 62531:2012(e) (IEEE Std 1850\u20132010): Standard for property specification language (PSL). IEC 62531:2012(E) (IEEE Std 1850\u20132010), pp. 1\u2013184, June 2012"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16"},{"issue":"4","key":"7_CR3","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/1713254.1713257","volume":"43","author":"L Ciortea","year":"2010","unstructured":"Ciortea, L., Zamfir, C., Bucur, S., Chipounov, V., Candea, G.: Cloud9: a software testing service. SIGOPS Oper. Syst. Rev. 43(4), 5\u201310 (2010)","journal-title":"SIGOPS Oper. Syst. Rev."},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-46017-9_1","volume-title":"Model Checking Software","author":"EM Clarke","year":"2002","unstructured":"Clarke, E.M.: SAT-based counterexample guided abstraction refinement. In: Bo\u0161na\u010dki, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, p. 1. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46017-9_1"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"EM Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52\u201371. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/BFb0025774"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"7_CR7","volume-title":"Temporal Logic and Temporal Logic Programming","author":"Z Duan","year":"2005","unstructured":"Duan, Z.: Temporal Logic and Temporal Logic Programming. Science Press, Beijing (2005)"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-88194-0_12","volume-title":"Formal Methods and Software Engineering","author":"Z Duan","year":"2008","unstructured":"Duan, Z., Tian, C.: A unified model checking approach with projection temporal logic. In: Liu, S., Maibaum, T., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 167\u2013186. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-88194-0_12"},{"key":"7_CR9","first-page":"340","volume":"5","author":"K Hao","year":"1990","unstructured":"Hao, K., Duan, Z.: Traceable automata. Chin. J. Comput. 5, 340\u2013348 (1990)","journal-title":"Chin. J. Comput."},{"issue":"5","key":"7_CR10","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1093\/logcom\/12.5.701","volume":"12","author":"Y Kesten","year":"1995","unstructured":"Kesten, Y., Pnueli, A.: A complete proof system for QPTL. J. Logic Comput. 12(5), 701\u2013745 (1995)","journal-title":"J. Logic Comput."},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Luke Ong, C.H.: A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In: IEEE Symposium on Logic in Computer Science, 2009. LICS 2009, pp. 179\u2013188 (2009)","DOI":"10.1109\/LICS.2009.29"},{"key":"7_CR12","unstructured":"Wang, M., Tian, C., Zhang, N., Duan, Z., Yao, C.: Translating C programs to MSVL programs. https:\/\/arxiv.org\/abs\/1809.00959 (2018)"},{"issue":"5","key":"7_CR13","doi-asserted-by":"publisher","first-page":"762","DOI":"10.1007\/s11704-016-6059-4","volume":"11","author":"X Wang","year":"2017","unstructured":"Wang, X., Tian, C., Duan, Z., Zhao, L.: MSVL: a typed language for temporal logic programming. Front. Comput. Sci. 11(5), 762\u2013785 (2017)","journal-title":"Front. Comput. Sci."},{"key":"7_CR14","doi-asserted-by":"publisher","unstructured":"Yang, K., Duan, Z., Tian, C., Zhang, N.: A compiler for MSVL and its applications. Theoretical Computer Science (2017). https:\/\/doi.org\/10.1016\/j.tcs.2017.07.032","DOI":"10.1016\/j.tcs.2017.07.032"},{"issue":"11","key":"7_CR15","doi-asserted-by":"publisher","first-page":"118101","DOI":"10.1007\/s11432-015-0882-6","volume":"59","author":"N Zhang","year":"2016","unstructured":"Zhang, N., Duan, Z., Tian, C.: Model checking concurrent systems with MSVL. SCI. CHINA Inf. Sci. 59(11), 118101 (2016)","journal-title":"SCI. CHINA Inf. Sci."}],"container-title":["Lecture Notes in Computer Science","Algorithmic Aspects in Information and Management"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-04618-7_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,13]],"date-time":"2024-03-13T13:57:43Z","timestamp":1710338263000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-04618-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030046170","9783030046187"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-04618-7_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"17 November 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"AAIM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Algorithmic Applications in Management","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dallas, TX","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 December 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 December 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aaim2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/aaim2018.wordpress.com\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}