{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T12:35:43Z","timestamp":1725885343912},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319577074"},{"type":"electronic","value":"9783319577081"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-57708-1_8","type":"book-chapter","created":{"date-parts":[[2017,4,20]],"date-time":"2017-04-20T12:03:37Z","timestamp":1492689817000},"page":"121-143","source":"Crossref","is-referenced-by-count":0,"title":["A Proof System for MSVL Programs in Coq"],"prefix":"10.1007","author":[{"given":"Lin","family":"Qian","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nan","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cong","family":"Tian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,21]]},"reference":[{"key":"8_CR1","series-title":"Contemporary Mathematics Series","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/029","volume-title":"Interactive Theorem Proving and Program Development","author":"W Bledsoe","year":"1984","unstructured":"Bledsoe, W., Loveland, D.: Interactive Theorem Proving and Program Development. Contemporary Mathematics Series, vol. 29. American Mathematical Society, Providence (1984)"},{"key":"8_CR2","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking, pp. 54\u201356. MIT Press, Cambridge (2000)"},{"key":"8_CR3","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). doi:\n10.1007\/978-3-540-88194-0_12"},{"issue":"4","key":"8_CR4","doi-asserted-by":"publisher","first-page":"572","DOI":"10.1109\/TCE.2015.7389814","volume":"61","author":"F Comert","year":"2015","unstructured":"Comert, F., Ovatman, T.: Attacking state space explosion problem in model checking embedded TV software. IEEE Trans. Consum. Electron. 61(4), 572\u2013579 (2015)","journal-title":"IEEE Trans. Consum. Electron."},{"issue":"1","key":"8_CR5","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/j.scico.2007.09.001","volume":"70","author":"Z Duan","year":"2008","unstructured":"Duan, Z., Yang, X., Koutny, M.: Frammed temporal logic programming. Sci. Comput. Program. 70(1), 31\u201361 (2008)","journal-title":"Sci. Comput. Program."},{"key":"8_CR6","unstructured":"Barras, B., Boutin, S., Cornes, C., et al.: The Coq proof assistant: reference manual. Rapport technique - INRIA (2000), \nhttps:\/\/coq.inria.fr"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-319-04915-1_5","volume-title":"Structured Object-Oriented Formal Language and Method","author":"X Wang","year":"2014","unstructured":"Wang, X., Duan, Z., Zhao, L.: Formalizing and implementing types in MSVL. In: Liu, S., Duan, Z. (eds.) SOFL+MSVL 2013. LNCS, vol. 8332, pp. 62\u201375. Springer, Cham (2014). doi:\n10.1007\/978-3-319-04915-1_5"},{"key":"8_CR8","unstructured":"Duan, Z.: An Extended Interval Temporal Logic and A Framing Technique for Temporal Logic Programming. Ph.D Thesis (Technical Report No. 556). University of Newcastle upon Tyne (1996)"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992). doi:\n10.1007\/3-540-55602-8_217"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BFb0031816","volume-title":"Formal Methods in Computer-Aided Design","author":"B Brock","year":"1996","unstructured":"Brock, B., Kaufmann, M., Moore, J.S.: ACL2 theorems about commercial microprocessors. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 275\u2013293. Springer, Heidelberg (1996). doi:\n10.1007\/BFb0031816"},{"key":"8_CR11","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","author":"M Gordon","year":"1993","unstructured":"Gordon, M., Melham, T.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/3-540-57826-9_160","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"S Kalvala","year":"1994","unstructured":"Kalvala, S.: Using isabelle to prove simple theorems. In: Joyce, J.J., Seger, C.-J.H. (eds.) HUG 1993. LNCS, vol. 780, pp. 514\u2013517. Springer, Heidelberg (1994). doi:\n10.1007\/3-540-57826-9_160"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/BFb0105410","volume-title":"Theorem Proving in Higher Order Logics","author":"DJ Howe","year":"1996","unstructured":"Howe, D.J.: Importing mathematics from HOL into Nuprl. In: Goos, G., Hartmanis, J., Leeuwen, J., Wright, J., Grundy, J., Harrison, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 267\u2013281. Springer, Heidelberg (1996). doi:\n10.1007\/BFb0105410"},{"issue":"1","key":"8_CR14","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 Comput. 27(1), 103\u2013131 (2015)","journal-title":"Formal Aspects Comput."},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-74591-4_3","volume-title":"Theorem Proving in Higher Order Logics","author":"AW Appel","year":"2007","unstructured":"Appel, A.W., Blazy, S.: Separation logic for small-step cminor. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 5\u201321. Springer, Heidelberg (2007). doi:\n10.1007\/978-3-540-74591-4_3"},{"key":"8_CR16","doi-asserted-by":"publisher","unstructured":"Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: Proceedings of the ACM SIGPLAN 2011 Conference on Programming Language Design and Implementation, vol. 47(6), pp. 234\u2013245 (2011)","DOI":"10.1145\/1993498.1993526"},{"issue":"5","key":"8_CR17","doi-asserted-by":"publisher","first-page":"865","DOI":"10.1017\/S0960129510000241","volume":"20","author":"X Yang","year":"2010","unstructured":"Yang, X., Duan, Z., Ma, Q.: Axiomatic semantics of projection temporal logic programs. Math. Struct. Comput. Sci. 20(5), 865\u2013914 (2010)","journal-title":"Math. Struct. Comput. Sci."},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/BFb0023729","volume-title":"Computer-Aided Verification","author":"A Valmari","year":"1991","unstructured":"Valmari, A.: A stubborn attack on state explosion. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 156\u2013165. Springer, Heidelberg (1991). doi:\n10.1007\/BFb0023729"},{"issue":"2","key":"8_CR19","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1006\/inco.1994.1035","volume":"110","author":"P Godefroid","year":"1994","unstructured":"Godefroid, P., Wolper, P.: A partial approach to model checking. Inf. Comput. 110(2), 305\u2013326 (1994)","journal-title":"Inf. Comput."},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-319-08783-2_7","volume-title":"Computing and Combinatorics","author":"N Zhang","year":"2014","unstructured":"Zhang, N., Duan, Z., Tian, C.: An axiomatization for cylinder computation model. In: Cai, Z., Zelikovsky, A., Bourgeois, A. (eds.) COCOON 2014. LNCS, vol. 8591, pp. 71\u201383. Springer, Cham (2014). doi:\n10.1007\/978-3-319-08783-2_7"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1007\/978-3-642-22616-8_36","volume-title":"Combinatorial Optimization and Applications","author":"N Zhang","year":"2011","unstructured":"Zhang, N., Duan, Z.: A semantic model for many-core parallel computing. In: Wang, W., Zhu, X., Du, D.-Z. (eds.) COCOA 2011. LNCS, vol. 6831, pp. 464\u2013479. Springer, Heidelberg (2011). doi:\n10.1007\/978-3-642-22616-8_36"},{"key":"8_CR22","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1016\/0167-6423(94)00019-0","volume":"23","author":"J Esparza","year":"1994","unstructured":"Esparza, J.: Model checking using net unfoldings. Sci. Comput. Program. 23, 151\u2013195 (1994)","journal-title":"Sci. Comput. Program."},{"key":"8_CR23","doi-asserted-by":"publisher","unstructured":"Ma, Y., Duan, Z., Wang, X.: An interpreter for framed tempura and its application. In: Proceedings of First Joint IEEE\/IFIP Symposium on Theoretical Aspects of Software Engineering, pp. 251\u2013260. IEEE Press (2007)","DOI":"10.1109\/TASE.2007.10"},{"key":"8_CR24","doi-asserted-by":"publisher","unstructured":"Borgstrom, J., Gordon, A., Pucella, R.: Roles, stacks, histories: a triple for hoare. In: Reflections on the Work of C.A.R. Hoare, pp. 71\u201399 (2010)","DOI":"10.1007\/978-1-84882-912-1_4"},{"issue":"5","key":"8_CR25","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1016\/j.tcs.2012.01.026","volume":"497","author":"Z Duan","year":"2013","unstructured":"Duan, Z., Zhang, N., Koutny, M.: A complete proof system for propositional projection temporal logic. Theoret. Comput. Sci. 497(5), 84\u2013107 (2013)","journal-title":"Theoret. Comput. Sci."},{"key":"8_CR26","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/s00236-007-0062-z","volume":"45","author":"C Tian","year":"2008","unstructured":"Tian, C., Duan, Z., Zhang, L.: A decision procedure for propositional projection temporal logic with infinite models. Acta Informatica 45, 43\u201378 (2008)","journal-title":"Acta Informatica"}],"container-title":["Lecture Notes in Computer Science","Structured Object-Oriented Formal Language and Method"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-57708-1_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,4,20]],"date-time":"2017-04-20T12:06:10Z","timestamp":1492689970000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-57708-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319577074","9783319577081"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-57708-1_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}