{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T07:16:51Z","timestamp":1725520611793},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540894384"},{"type":"electronic","value":"9783540894391"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"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":[[2008]]},"DOI":"10.1007\/978-3-540-89439-1_22","type":"book-chapter","created":{"date-parts":[[2008,11,14]],"date-time":"2008-11-14T22:03:10Z","timestamp":1226700190000},"page":"305-317","source":"Crossref","is-referenced-by-count":4,"title":["On Bounded Reachability of Programs with Set Comprehensions"],"prefix":"10.1007","author":[{"given":"Margus","family":"Veanes","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ando","family":"Saabas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/11691617_9","volume-title":"Model Checking Software","author":"A. Armando","year":"2006","unstructured":"Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using SMT solvers instead of SAT solvers. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol.\u00a03925, pp. 146\u2013162. Springer, Heidelberg (2006)"},{"issue":"2","key":"22_CR2","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1016\/S0890-5401(03)00020-8","volume":"183","author":"A. Armando","year":"2003","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Inf. Comput.\u00a0183(2), 140\u2013164 (2003)","journal-title":"Inf. Comput."},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"22_CR4","unstructured":"B\u00e8s, A.: A survey of arithmetical definability, A tribute to Maurice Boffa, Special Issue of Belg. Math. Soc., 1\u201354 (2002)"},{"key":"22_CR5","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., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"22_CR6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59207-2","volume-title":"The Classical Decision Problem","author":"E. B\u00f6rger","year":"1997","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The Classical Decision Problem. Springer, Heidelberg (1997)"},{"key":"22_CR7","unstructured":"Bouillaguet, C., Kuncak, V., Wies, T., Zee, K., Rinard, M.: On using first-order theorem provers in the Jahob data structure verification system. Technical Report MIT-CSAIL-TR-2006-072, Massachusetts Institute of Technology (November 2006)"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2006","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 427\u2013442. Springer, Heidelberg (2006)"},{"key":"22_CR9","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.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963. Springer, Heidelberg (2008)"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/3-540-45620-1_35","volume-title":"Automated Deduction - CADE-18","author":"L.M. Moura de","year":"2002","unstructured":"de Moura, L.M., Rue\u00df, H., Sorea, M.: Lazy theorem proving for bounded model checking over infinite domains. In: Voronkov, A. (ed.) CADE 2002. LNCS, vol.\u00a02392, pp. 438\u2013455. Springer, Heidelberg (2002)"},{"key":"22_CR12","unstructured":"Fischer, M.J., Rabin, M.O.: Super-exponential complexity of Presburger arithmetic. In: SIAMAMS, pp. 27\u201341 (1974)"},{"issue":"4","key":"22_CR13","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1145\/566171.566190","volume":"27","author":"W. Grieskamp","year":"2002","unstructured":"Grieskamp, W., Gurevich, Y., Schulte, W., Veanes, M.: Generating finite state machines from abstract state machines. SIGSOFT Softw. Eng. Notes\u00a027(4), 112\u2013122 (2002)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Grieskamp, W., MacDonald, D., Kicillof, N., Nandan, A., Stobie, K., Wurden, F.: Model-based quality assurance of Windows protocol documentation. In: ICST 2008, Lillehammer, Norway (April 2008)","DOI":"10.1109\/ICST.2008.50"},{"key":"22_CR15","first-page":"9","volume-title":"Specification and Validation Methods","author":"Y. Gurevich","year":"1995","unstructured":"Gurevich, Y.: Evolving Algebras 1993: Lipari Guide. In: Specification and Validation Methods, pp. 9\u201336. Oxford University Press, Oxford (1995)"},{"issue":"3","key":"22_CR16","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1016\/j.tcs.2005.06.017","volume":"343","author":"Y. Gurevich","year":"2005","unstructured":"Gurevich, Y., Rossman, B., Schulte, W.: Semantic essence of AsmL. Theor. Comput. Sci.\u00a0343(3), 370\u2013412 (2005)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"22_CR17","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1006\/inco.1999.2797","volume":"152","author":"Y. Gurevich","year":"1999","unstructured":"Gurevich, Y., Veanes, M.: Logic with equality: partisan corroboration and shifted pairing. Inf. Comput.\u00a0152(2), 205\u2013235 (1999)","journal-title":"Inf. Comput."},{"issue":"1","key":"22_CR18","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.tcs.2007.01.009","volume":"376","author":"Y. Gurevich","year":"2007","unstructured":"Gurevich, Y., Veanes, M., Wallace, C.: Can abstract state machines be useful in language theory? Theor. Comput. Sci.\u00a0376(1), 17\u201329 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"22_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_33","volume-title":"Foundations of Software Science and Computational Structures","author":"P. Habermehl","year":"2008","unstructured":"Habermehl, P., Iosif, R., Vojnar, T.: What else is decidable about arrays? In: Amadio, R. (ed.) FOSSACS 2008. LNCS, vol.\u00a04962. Springer, Heidelberg (2008)"},{"key":"22_CR20","volume-title":"Model theory","author":"W. Hodges","year":"1995","unstructured":"Hodges, W.: Model theory. Cambridge Univ. Press, Cambridge (1995)"},{"key":"22_CR21","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"J.E. Hopcroft","year":"1979","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)"},{"key":"22_CR22","volume-title":"Model-based Software Testing and Analysis with C#","author":"J. Jacky","year":"2008","unstructured":"Jacky, J., Veanes, M., Campbell, C., Schulte, W.: Model-based Software Testing and Analysis with C#. Cambridge University Press, Cambridge (2008)"},{"issue":"8","key":"22_CR23","first-page":"39","volume":"174","author":"S. Jacobs","year":"2007","unstructured":"Jacobs, S., Sofronie-Stokkermans, V.: Applications of hierarchical reasoning in the verification of complex systems. ENTCS\u00a0174(8), 39\u201354 (2007)","journal-title":"ENTCS"},{"key":"22_CR24","first-page":"105","volume-title":"SIGSOFT FSE 2006","author":"D. Kapur","year":"2006","unstructured":"Kapur, D., Majumdar, R., Zarba, C.G.: Interpolation for data structures. In: SIGSOFT FSE 2006, pp. 105\u2013116. ACM, New York (2006)"},{"key":"22_CR25","unstructured":"Kapur, D., Zarba, C.G.: A reduction approach to decision procedures (2006)"},{"key":"22_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/11532231_20","volume-title":"Automated Deduction \u2013 CADE-20","author":"V. Kuncak","year":"2005","unstructured":"Kuncak, V., Nguyen, H.H., Rinard, M.: An algorithm for deciding BAPA: Boolean algebra with Presburger arithmetic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol.\u00a03632, pp. 260\u2013277. Springer, Heidelberg (2005)"},{"key":"22_CR27","unstructured":"Leino, R., Monahan, R.: Automatic verification of textbook programs that use comprehensions. In: FTfJP 2007, Berlin, Germany (July 2007)"},{"key":"22_CR28","volume-title":"Hilbert\u2019s tenth problem","author":"Y.V. Matiyasevich","year":"1993","unstructured":"Matiyasevich, Y.V.: Hilbert\u2019s tenth problem. MIT Press, Cambridge (1993)"},{"issue":"2","key":"22_CR29","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst.\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"22_CR30","unstructured":"NModel. Public version released (May 2008), http:\/\/www.codeplex.com\/NModel"},{"key":"22_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-540-78163-9_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R. Piskac","year":"2008","unstructured":"Piskac, R., Kuncak, V.: Decision procedures for multisets with cardinality constraints. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol.\u00a04905, pp. 218\u2013232. Springer, Heidelberg (2008)"},{"key":"22_CR32","unstructured":"Piskac, R., Kuncak, V.: On Linear Arithmetic with Stars. Technical Report LARA-REPORT-2008-005, EPFL (2008)"},{"key":"22_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-540-39866-0_24","volume-title":"Perspectives of System Informatics","author":"T. Rybina","year":"2004","unstructured":"Rybina, T., Voronkov, A.: A logical reconstruction of reachability. In: Broy, M., Zamulin, A.V. (eds.) PSI 2003. LNCS, vol.\u00a02890, pp. 222\u2013237. Springer, Heidelberg (2004)"},{"key":"22_CR34","unstructured":"SMB2 (2008), http:\/\/msdn2.microsoft.com\/en-us\/library\/cc246482.aspx"},{"key":"22_CR35","first-page":"29","volume-title":"LICS 2001","author":"A. Stump","year":"2001","unstructured":"Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for an extensional theory of arrays. In: LICS 2001, pp. 29\u201337. IEEE, Los Alamitos (2001)"},{"key":"22_CR36","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2008","author":"M. Veanes","year":"2008","unstructured":"Veanes, M., Bj\u00f8rner, N., Raschke, A.: An SMT approach to bounded reachability analysis of model programs. In: Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds.) FORTE 2008. LNCS, vol.\u00a05048. Springer, Heidelberg (2008)"},{"key":"22_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-540-78917-8_2","volume-title":"Formal Methods and Testing","author":"M. Veanes","year":"2008","unstructured":"Veanes, M., Campbell, C., Grieskamp, W., Schulte, W., Tillmann, N., Nachmanson, L.: Model-based testing of object-oriented reactive systems with Spec Explorer. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) FORTEST 2008. LNCS, vol.\u00a04949, pp. 39\u201376. Springer, Heidelberg (2008)"},{"key":"22_CR38","doi-asserted-by":"crossref","unstructured":"Veanes, M., Saabas, A., Bj\u00f8rner, N.: Bounded reachability of model programs. Technical Report MSR-TR-2008-81, Microsoft Research (May 2008)","DOI":"10.1007\/978-3-540-89439-1_22"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-89439-1_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T09:12:26Z","timestamp":1557911546000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-89439-1_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540894384","9783540894391"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-89439-1_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}