{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T02:03:37Z","timestamp":1725501817041},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540779643"},{"type":"electronic","value":"9783540779667"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-77966-7_17","type":"book-chapter","created":{"date-parts":[[2008,2,1]],"date-time":"2008-02-01T08:59:24Z","timestamp":1201856364000},"page":"202-217","source":"Crossref","is-referenced-by-count":2,"title":["A Complete Bounded Model Checking Algorithm for Pushdown Systems"],"prefix":"10.1007","author":[{"given":"G\u00e9rard","family":"Basler","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]},{"given":"Georg","family":"Weissenbacher","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","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.\u00a01885, pp. 113\u2013130. Springer, Heidelberg (2000)"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/b98210","volume-title":"Integrated Formal Methods","author":"T. Ball","year":"2004","unstructured":"Ball, T., et al.: SLAM and Static Driver Verifier: Technology transfer of formal methods inside Microsoft. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol.\u00a02999, pp. 1\u201320. Springer, Heidelberg (2004)"},{"key":"17_CR3","first-page":"189","volume-title":"Program Flow Analysis: Theory and Applications","author":"M. Sharir","year":"1981","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural dataflow analysis. In: Program Flow Analysis: Theory and Applications, pp. 189\u2013233. Prentice-Hall, Englewood Cliffs (1981)"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. In: Workshop on Verification of Infinite State Systems (INFINITY). ENTCS, vol.\u00a09, pp. 27\u201339 (1997)","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"17_CR5","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.\u00a01855, pp. 232\u2013247. Springer, Heidelberg (2000)"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-540-73370-6_10","volume-title":"Model Checking Software","author":"G. Basler","year":"2007","unstructured":"Basler, G., Kroening, D., Weissenbacher, G.: SAT-based summarisation for Boolean programs. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 131\u2013148. Springer, Heidelberg (2007)"},{"key":"17_CR7","unstructured":"Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2002)"},{"key":"17_CR8","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/BF01969548","volume":"6","author":"J.R. B\u00fcchi","year":"1964","unstructured":"B\u00fcchi, J.R.: Regular canonical systems. Archive for Mathematical Logic\u00a06, 91 (1964)","journal-title":"Archive for Mathematical Logic"},{"key":"17_CR9","unstructured":"Ball, T., Rajamani, S.: Boolean programs: A model and process for software analysis. Technical Report 2000-14, Microsoft Research (2000)"},{"key":"17_CR10","first-page":"203","volume-title":"Programming Language Design and Implementation (PLDI)","author":"T. Ball","year":"2001","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Programming Language Design and Implementation (PLDI), pp. 203\u2013213. ACM Press, New York (2001)"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","first-page":"104","volume-title":"Model Checking Software","author":"K.R.M. Leino","year":"2003","unstructured":"Leino, K.R.M.: A SAT characterization of Boolean-program correctness. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 104\u2013120. Springer, Heidelberg (2003)"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/3-540-36384-X_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Kroening","year":"2002","unstructured":"Kroening, D., Strichman, O.: Efficient computation of recurrence diameters. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 298\u2013309. Springer, Heidelberg (2002)"},{"key":"17_CR15","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 Transactions on Programming Languages and Systems (TOPLAS)\u00a027, 786\u2013818 (2005)","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.\u00a03639, pp. 75\u201390. Springer, Heidelberg (2005)"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Qadeer","year":"2005","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 93\u2013107. Springer, Heidelberg (2005)"},{"key":"17_CR18","series-title":"ENTCS","volume-title":"Verification of Infinite State Systems (INFINITY)","author":"T. Touili","year":"2006","unstructured":"Touili, T., Sighireanu, M.: Bounded communication reachability analysis of process rewrite systems with ordered parallelism. In: Verification of Infinite State Systems (INFINITY). ENTCS, Elsevier, Amsterdam (2006)"},{"key":"17_CR19","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1109\/FMCAD.2006.24","volume-title":"Formal Methods in Computer-Aided Design FMCAD","author":"B. Cook","year":"2006","unstructured":"Cook, B., Kroening, D., Sharygina, N.: Over-Approximating Boolean Programs with unbounded thread creation. In: Formal Methods in Computer-Aided Design FMCAD, pp. 53\u201359. IEEE Computer Society Press, Los Alamitos (2006)"},{"key":"17_CR20","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1145\/604131.604137","volume-title":"Principles of Programming Languages (POPL)","author":"A. Bouajjani","year":"2003","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: Principles of Programming Languages (POPL), pp. 62\u201373. ACM Press, New York (2003)"},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/11817963_32","volume-title":"Computer Aided Verification","author":"A. Lal","year":"2006","unstructured":"Lal, A., Reps, T.: Improving pushdown system model checking. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 343\u2013357. Springer, Heidelberg (2006)"},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11805618_11","volume-title":"Term Rewriting and Applications","author":"A. Bouajjani","year":"2006","unstructured":"Bouajjani, A., Esparza, J.: Rewriting models of Boolean programs. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, Springer, Heidelberg (2006)"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Xie, Y., Aiken, A.: Saturn: A scalable framework for error detection using boolean satisfiability. ACM Transactions on Programming Languages and Systems (TOPLAS)\u00a029 (2007)","DOI":"10.1145\/1232420.1232423"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-77966-7_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:57:25Z","timestamp":1619521045000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-77966-7_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540779643","9783540779667"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-77966-7_17","relation":{},"subject":[]}}