{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T12:35:49Z","timestamp":1725885349377},"publisher-location":"Cham","reference-count":33,"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_11","type":"book-chapter","created":{"date-parts":[[2017,4,20]],"date-time":"2017-04-20T08:03:37Z","timestamp":1492675417000},"page":"181-200","source":"Crossref","is-referenced-by-count":0,"title":["SMT-based Bounded Model Checking for Cooperative Software with a Deterministic Scheduler"],"prefix":"10.1007","author":[{"given":"Haitao","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yonggang","family":"Lu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,21]]},"reference":[{"key":"11_CR1","unstructured":"IEEE 1666: SystemC language Reference Manual (2005)"},{"issue":"11","key":"11_CR2","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/1592761.1592781","volume":"152","author":"EM Clarke","year":"2009","unstructured":"Clarke, E.M., Emerson, E.A., et al.: Model checking: algorithmic verification and debugging. Commun. ACM 152(11), 74\u201384 (2009)","journal-title":"Commun. ACM"},{"key":"11_CR3","volume-title":"Real-Time Systems and Programming Languages","author":"A Burns","year":"2009","unstructured":"Burns, A., Wellings, A.: Real-Time Systems and Programming Languages, 4th edn. Addison Wesley Longman, New York (2009)","edition":"4"},{"key":"11_CR4","unstructured":"Cimatti, A., Micheli, A., Narasamdya, I., Roveri, M.: Verifying SystemC: a software model checking approach. In: FMCAD, pp. 51\u201359 (2010)"},{"issue":"1","key":"11_CR5","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s10009-008-0091-0","volume":"11","author":"A Alessandro","year":"2009","unstructured":"Alessandro, A., Jacopo, M., Lorenzo, P.: Bounded model checking of software using SMT solvers instead of SAT solvers. Int. J. Softw. Tools Technol. Transf. (STTT) 11(1), 69\u201383 (2009)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"key":"11_CR6","unstructured":"Cimatti, A., Micheli, A., Narasamdya, I., Roveri, M.: Kratos Homepage (2010). https:\/\/es-static.fbk.eu\/tools\/kratos\/"},{"issue":"11","key":"11_CR7","first-page":"117","volume":"58","author":"B Armin","year":"2003","unstructured":"Armin, B., Clarke, E.M., Zhu, Y.: Bounded model checking. Adv. Comput. 58(11), 117\u2013148 (2003)","journal-title":"Adv. Comput."},{"key":"11_CR8","first-page":"1278","volume":"13","author":"VR Basili","year":"1987","unstructured":"Basili, V.R., Selby, R.W.: Comparing the effectiveness of software testing strategies. TSE 13, 1278\u20131296 (1987)","journal-title":"TSE"},{"key":"11_CR9","doi-asserted-by":"publisher","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on UPPAAL. In: Formal Methods for the Design of Real-Time Systems: 4th International School on Formal Methods for the Design of Computer Communication, and Software Systems, pp. 200\u2013236 (2004)","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"11_CR10","doi-asserted-by":"publisher","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: POPL, pp. 110\u2013121 (2005)","DOI":"10.1145\/1040305.1040315"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-540-73370-6_14","volume-title":"Model Checking Software","author":"C Traulsen","year":"2007","unstructured":"Traulsen, C., Cornet, J., Moy, M., Maraninchi, F.: A SystemC\/TLM semantics in Promela and its possible applications. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 204\u2013222. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-73370-6_14"},{"key":"11_CR12","doi-asserted-by":"publisher","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: An efficient method of computing static single assignment form. In: POPL, pp. 25\u201335 (1989)","DOI":"10.1145\/75277.75280"},{"key":"11_CR13","doi-asserted-by":"publisher","unstructured":"Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: FMCAD, pp. 25\u201332 (2009)","DOI":"10.1109\/FMCAD.2009.5351147"},{"key":"11_CR14","doi-asserted-by":"publisher","unstructured":"Kroening, D., Sharygina, N.: Formal verification of SystemC by automatic hardware\/software partitioning. In: MEMOCODE, pp. 101\u2013110 (2005)","DOI":"10.1109\/MEMCOD.2005.1487900"},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"Tabakov, D., Kamhi, G., Vardi, M.Y., Singerman, E.: A temporal language for SystemC. In: FMCAD, pp. 1\u20139 (2008)","DOI":"10.1109\/FMCAD.2008.ECP.26"},{"key":"11_CR16","unstructured":"Kroening, D., Clarke, E., et al.: The CBMC Homepage (2004). http:\/\/www.cprover.org\/cbmc\/"},{"key":"11_CR17","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)"},{"issue":"1","key":"11_CR18","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/s00236-007-0062-z","volume":"45","author":"Z Duan","year":"2008","unstructured":"Duan, Z., Tian, C., Zhang, L.: A decision procedure for propositional projection temporal logic with infinite models. Acta Informatica 45(1), 43\u201378 (2008)","journal-title":"Acta Informatica"},{"issue":"1","key":"11_CR19","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.: Framed temporal logic programming. Sci. Comput. Program. 70(1), 31\u201361 (2008)","journal-title":"Sci. Comput. Program."},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24730-2_15"},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SATBased predicate abstraction for ANSI-C. In: TACAS, pp. 570\u2013574 (2005)","DOI":"10.1007\/978-3-540-31980-1_40"},{"issue":"5","key":"11_CR22","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. (TOPLAS) 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"11_CR23","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"GJ Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Lucent Technologies Inc., Bell Laboratories, Boston (2003)"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"George, C.N., Scott, M., Shree, P.R., Westley, W.: CIL: intermediate language and tools for analysis and transformation of C programs. In: Proceedings of the 11th International Conference on Compiler Construction, pp. 213\u2013228 (2002)","DOI":"10.1007\/3-540-45937-5_16"},{"key":"11_CR25","doi-asserted-by":"publisher","unstructured":"Zhang, H., Aoki, T., et al.: SMT-based bounded model checking for OSEK\/VDX applications. In: 20th APSEC, pp. 307\u2013314 (2013)","DOI":"10.1109\/APSEC.2013.49"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Zhang, H., Aoki, T., Chiba, Y.: A spin-based approach for checking OSEK\/VDX applications. In: 3rd International Workshop FTSCS in ICFEM, pp. 239\u2013255 (2014)","DOI":"10.1007\/978-3-319-17581-2_16"},{"key":"11_CR27","doi-asserted-by":"publisher","unstructured":"Cordeiro, L., Fischer, B.: Verifying multi-threaded software using SMT-based context-bounded model checking. In: ICSE 2011, vol. 3(9), pp. 331\u2013340, May 2011","DOI":"10.1145\/1985793.1985839"},{"issue":"1","key":"11_CR28","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/s11241-007-9036-z","volume":"38","author":"L Waszniowski","year":"2008","unstructured":"Waszniowski, L., Hanzlek, Z.: Formal verification of multitasking applications based on timed automata model. Real-Time Syst. 38(1), 39\u201365 (2008)","journal-title":"Real-Time Syst."},{"key":"11_CR29","unstructured":"Lemieux, J.: Programming in the OSEK\/VDX environment. CMP, Suite 200 Lawrence, KS 66046, USA (2001)"},{"key":"11_CR30","unstructured":"de Moura, L., Passmore, G.: Z3 Homepage. http:\/\/z3.codeplex.com\/"},{"key":"11_CR31","doi-asserted-by":"publisher","unstructured":"Blanc, N., Kroening, D.: Race analysis for SystemC using model checking. In: ICCAD, pp. 356\u2013363 (2008)","DOI":"10.1109\/ICCAD.2008.4681598"},{"key":"11_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/978-3-540-78800-3_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Blanc","year":"2008","unstructured":"Blanc, N., Kroening, D., Sharygina, N.: Scoot: a tool for the analysis of SystemC models. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 467\u2013470. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78800-3_36"},{"key":"11_CR33","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1016\/j.tcs.2011.12.014","volume":"461","author":"C Tian","year":"2012","unstructured":"Tian, C., Duan, Z., Zhang, N.: An efficient approach for abstraction-refinement in model checking. Theor. Comput. Sci. 461, 76\u201385 (2012)","journal-title":"Theor. Comput. Sci."}],"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_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,21]],"date-time":"2019-09-21T07:23:39Z","timestamp":1569050619000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-57708-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319577074","9783319577081"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-57708-1_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}