{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:28:24Z","timestamp":1742912904925,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661964"},{"type":"electronic","value":"9783319661971"}],"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-66197-1_20","type":"book-chapter","created":{"date-parts":[[2017,8,11]],"date-time":"2017-08-11T21:02:30Z","timestamp":1502485350000},"page":"316-331","source":"Crossref","is-referenced-by-count":1,"title":["IJIT: An API for Boolean Program Analysis with Just-in-Time Translation"],"prefix":"10.1007","author":[{"given":"Peizun","family":"Liu","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Wahl","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,13]]},"reference":[{"issue":"4","key":"20_CR1","doi-asserted-by":"publisher","first-page":"457","DOI":"10.2178\/bsl\/1294171129","volume":"16","author":"PA Abdulla","year":"2010","unstructured":"Abdulla, P.A.: Well (and better) quasi-ordered transition systems. Bull. Symbolic Logic 16(4), 457\u2013515 (2010)","journal-title":"Bull. Symbolic Logic"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.K.: General decidability theorems for infinite-state systems. In: LICS, pp. 313\u2013321 (1996)","DOI":"10.1109\/LICS.1996.561359"},{"issue":"4","key":"20_CR3","doi-asserted-by":"publisher","first-page":"786","DOI":"10.1145\/1075382.1075387","volume":"27","author":"R Alur","year":"2005","unstructured":"Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T., Yannakakis, M.: Analysis of recursive state machines. ACM Trans. Program. Lang. Syst. 27(4), 786\u2013818 (2005)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"20_CR4","unstructured":"Ball, T., Rajamani, S.: Boolean programs: a model and process for software analysis. Technical report MSR-TR-2000-14, Microsoft Research (2000)"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/10722468_7","volume-title":"SPIN Model Checking and Software Verification","author":"T Ball","year":"2000","unstructured":"Ball, T., Rajamani, S.K.: Bebop: a symbolic model checker for boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 113\u2013130. Springer, Heidelberg (2000). doi:\n10.1007\/10722468_7"},{"issue":"1","key":"20_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/565816.503274","volume":"37","author":"Thomas Ball","year":"2002","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: POPL, pp. 1\u20133 (2002)","journal-title":"ACM SIGPLAN Notices"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-642-12002-2_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Basler","year":"2010","unstructured":"Basler, G., Hague, M., Kroening, D., Ong, C.-H.L., Wahl, T., Zhao, H.: Boom: taking boolean program model checking one step further. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 145\u2013149. Springer, Heidelberg (2010). doi:\n10.1007\/978-3-642-12002-2_11"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1007\/978-3-540-31980-1_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2005","unstructured":"Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 570\u2013574. Springer, Heidelberg (2005). doi:\n10.1007\/978-3-540-31980-1_40"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/11537328_9","volume-title":"Model Checking Software","author":"B Cook","year":"2005","unstructured":"Cook, B., Kroening, D., Sharygina, N.: Symbolic model checking for asynchronous boolean programs. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 75\u201390. Springer, Heidelberg (2005). doi:\n10.1007\/11537328_9"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/3-540-46002-0_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Delzanno","year":"2002","unstructured":"Delzanno, G., Raskin, J.-F., Begin, L.: Towards the automated verification of multithreaded Java programs. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 173\u2013187. Springer, Heidelberg (2002). doi:\n10.1007\/3-540-46002-0_13"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/10722167_20","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2000","unstructured":"Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 232\u2013247. Springer, Heidelberg (2000). doi:\n10.1007\/10722167_20"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/3-540-44585-4_30","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2001","unstructured":"Esparza, J., Schwoon, S.: A BDD-based model checker for recursive programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 324\u2013336. Springer, Heidelberg (2001). doi:\n10.1007\/3-540-44585-4_30"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72\u201383. Springer, Heidelberg (1997). doi:\n10.1007\/3-540-63166-6_10"},{"issue":"5","key":"20_CR14","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker Spin. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1007\/978-3-642-14295-6_55","volume-title":"Computer Aided Verification","author":"A Kaiser","year":"2010","unstructured":"Kaiser, A., Kroening, D., Wahl, T.: Dynamic cutoff detection in parameterized concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 645\u2013659. Springer, Heidelberg (2010). doi:\n10.1007\/978-3-642-14295-6_55"},{"issue":"2","key":"20_CR16","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/S0022-0000(69)80011-5","volume":"3","author":"RM Karp","year":"1969","unstructured":"Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147\u2013195 (1969)","journal-title":"J. Comput. Syst. Sci."},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"La Torre, S., Parthasarathy, M., Parlato, G.: Analyzing recursive programs using a fixed-point calculus. In: PLDI, pp. 211\u2013222 (2009)","DOI":"10.1145\/1542476.1542500"},{"key":"20_CR18","unstructured":"Liu, P.: \nhttp:\/\/www.ccs.neu.edu\/home\/lpzun\/ijit\/"},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"Liu, P., Wahl, T.: Infinite-state backward exploration of Boolean broadcast programs. In: FMCAD, pp. 155\u2013162 (2014)","DOI":"10.1109\/FMCAD.2014.6987608"},{"key":"20_CR20","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-319-66197-1_20","volume-title":"Software Engineering and Formal Methods","author":"Peizun Liu","year":"2017","unstructured":"Liu, P., Wahl, T.: IJIT: an API for Boolean program analysis with just-in-time translation (extended technical report) (2017). CoRR \narXiv.org\/abs\/1706.03167"},{"issue":"2","key":"20_CR21","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203\u2013232 (2003)","journal-title":"Autom. Softw. Eng."}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66197-1_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,7,24]],"date-time":"2018-07-24T23:54:08Z","timestamp":1532476448000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66197-1_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661964","9783319661971"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66197-1_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}