{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T02:41:46Z","timestamp":1743129706268,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319213972"},{"type":"electronic","value":"9783319213989"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21398-9_41","type":"book-chapter","created":{"date-parts":[[2015,6,23]],"date-time":"2015-06-23T15:12:41Z","timestamp":1435072361000},"page":"521-533","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Model Checking MSVL Programs Based on Dynamic Symbolic Execution"],"prefix":"10.1007","author":[{"given":"Zhenhua","family":"Duan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kangkang","family":"Bu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cong","family":"Tian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nan","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,6,24]]},"reference":[{"issue":"1","key":"41_CR1","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/s00165-014-0303-1","volume":"27","author":"Q Ma","year":"2015","unstructured":"Ma, Q., Duan, Z., Zhang, N., Wang, X.: Verification of distributed systems with the axiomatic system of MSVL. Formal Aspects of Computing 27(1), 103\u2013131 (2015)","journal-title":"Formal Aspects of Computing"},{"key":"41_CR2","doi-asserted-by":"crossref","unstructured":"King, J.C.: Symbolic Execution and Program Testing. Journal of ACM, 385\u2013394 (1976)","DOI":"10.1145\/360248.360252"},{"key":"41_CR3","doi-asserted-by":"crossref","unstructured":"Ma, Y., Duan, Z., Wang, X., Yang, X.: An Interpreter for framed tempura and its application. In: Proceedings TASE 2007, pp. 251\u2013260 (2007)","DOI":"10.1109\/TASE.2007.10"},{"key":"41_CR4","doi-asserted-by":"crossref","unstructured":"Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: Exe: automatically generating inputs of death. In: Proceedings of CCS 2006, pp. 322\u2013335 (2006)","DOI":"10.1145\/1180405.1180445"},{"key":"41_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","volume-title":"Verification of Object-Oriented Software","author":"B Beckert","year":"2007","unstructured":"Beckert, B., Hahnle, R., Schmitt, P.H.: Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)"},{"key":"41_CR6","unstructured":"Jacobs, B., Piessens, F.: The Verifast Program Verifier (2008)"},{"key":"41_CR7","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Proceedings of PLDI 2005, pp. 213\u2013223 (2010)","DOI":"10.1145\/1064978.1065036"},{"key":"41_CR8","volume-title":"Temporal Logic and Temporal Logic Programming","author":"Z Duan","year":"2006","unstructured":"Duan, Z.: Temporal Logic and Temporal Logic Programming. Science Press, Beijing (2006)"},{"key":"41_CR9","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Proceedings of ESEC FSE 2005, pp. 263C\u2013272 (2005)","DOI":"10.1145\/1095430.1081750"},{"key":"41_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"454","DOI":"10.1007\/978-3-642-04244-7_37","volume-title":"Principles and Practice of Constraint Programming - CP 2009","author":"J Jaffar","year":"2009","unstructured":"Jaffar, J., Santosa, A.E., Voicu, R.: An interpolation method for CLP traversal. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 454\u2013469. Springer, Heidelberg (2009)"},{"key":"41_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-642-14295-6_10","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2010","unstructured":"McMillan, K.L.: Lazy annotation for program testing and verification. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 104\u2013118. Springer, Heidelberg (2010)"},{"key":"41_CR12","doi-asserted-by":"crossref","unstructured":"Harris, W.R., Sankaranarayanan, S., Ivan\u010di\u0107, F., Gupta, A.: Program analysis via satisfiability modulo path programs. In: Proceedings of POPL 2010, pp. 71\u201382 (2010)","DOI":"10.1145\/1707801.1706309"},{"key":"41_CR13","unstructured":"Duan, Z.: An extended interval temporal logic and a framing technique for temporal logic programming, Ph.D. thesis, University of Newcastle upon Tyne (1996)"},{"key":"41_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: CounterrExample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"41_CR15","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proceedings of PLDI 2001, pp. 203\u2013213 (2001)","DOI":"10.1145\/378795.378846"},{"key":"41_CR16","doi-asserted-by":"crossref","unstructured":"Zhang, Y., Chen, Z., Wang, J., Dongy, W., Liu, Z.: Regular property guided dynamic symbolic execution. In: Proceedings of ICSE 2015 (2015)","DOI":"10.1109\/ICSE.2015.80"},{"key":"41_CR17","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems-specification. Springer (1992). ISBN 978-3-540-97664-6","DOI":"10.1007\/978-1-4612-0931-7_1"},{"key":"41_CR18","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Bounded model checking. Advances in computers 58, 117\u2013148 (2003)","journal-title":"Advances in computers"},{"key":"41_CR19","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/j.entcs.2014.12.005","volume":"309","author":"K Yang","year":"2014","unstructured":"Yang, K., Duan, Z., Tian, C.: Modeling and Verification of REC Handover Protocol. Electronic Notes Theoretical Computer Science 309, 51\u201362 (2014)","journal-title":"Electronic Notes Theoretical Computer Science"},{"key":"41_CR20","doi-asserted-by":"crossref","unstructured":"Duan, Z., Tian, C.: A unified model checking approach with projection temporal logic. In: Proceedings of ICFEM 2008, pp. 167\u2013186 (2008)","DOI":"10.1007\/978-3-540-88194-0_12"},{"key":"41_CR21","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/j.tcs.2014.02.011","volume":"554","author":"Z Duan","year":"2014","unstructured":"Duan, Z., Tian, C.: A practical decision procedure for Propositional Projection Temporal Logic with infinite models. Theoretical Computer Science 554, 169\u2013190 (2014)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Computing and Combinatorics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21398-9_41","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T02:27:19Z","timestamp":1676946439000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21398-9_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319213972","9783319213989"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21398-9_41","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"24 June 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}