{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T05:21:56Z","timestamp":1737436916143,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540733676"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73368-3_50","type":"book-chapter","created":{"date-parts":[[2007,8,29]],"date-time":"2007-08-29T22:29:34Z","timestamp":1188426574000},"page":"491-503","source":"Crossref","is-referenced-by-count":10,"title":["Leaping Loops in the Presence of Abstraction"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Ball","sequence":"first","affiliation":[]},{"given":"Orna","family":"Kupferman","sequence":"additional","affiliation":[]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"50_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T.: A theory of predicate-complete test coverage and generation. In: 3rd International Symposium on Formal Methods for Components and Objects (2004)","DOI":"10.1007\/11561163_1"},{"key":"50_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S.K., Ustuner, A.: Thorough static analysis of device drivers. In: EuroSys (2006)","DOI":"10.1145\/1217935.1217943"},{"key":"50_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T. Ball","year":"2005","unstructured":"Ball, T., Kupferman, O.: Better under-approximation of programs by hiding of variables. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, Springer, Heidelberg (2005)"},{"key":"50_CR4","doi-asserted-by":"crossref","unstructured":"Berdine, J., Chawdhary, A., Cook, B., Distefano, D., O\u2019Hearn, P.: Variance analyses from invariance analyses. In: Proc. 34th POPL (2007)","DOI":"10.1145\/1190216.1190249"},{"key":"50_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1007\/11513988_48","volume-title":"Computer Aided Verification","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.: Linear Ranking with Reachability. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 491\u2013504. Springer, Heidelberg (2005)"},{"key":"50_CR6","first-page":"415","volume-title":"Proc. ACM PLDI","author":"B. Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Proc. ACM PLDI, pp. 415\u2013426. ACM Press, New York (2006)"},{"key":"50_CR7","first-page":"238","volume-title":"Proc. 4th POPL","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In: Proc. 4th POPL, pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"50_CR8","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"50_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/3-540-45657-0_11","volume-title":"Computer Aided Verification","author":"P. Godefroid","year":"2002","unstructured":"Godefroid, P., Jagadeesan, R.: Automatic abstraction using generalized model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 137\u2013150. Springer, Heidelberg (2002)"},{"key":"50_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/11817963_16","volume-title":"Computer Aided Verification","author":"D. Kroening","year":"2006","unstructured":"Kroening, D., Weissenbacher, G.: Counterexamples with loops for predicate abstraction. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 152\u2013165. Springer, Heidelberg (2006)"},{"key":"50_CR11","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Thomsen, G.B.: A modal process logic. In: Proc. 3th LICS\u00a0(1988)","DOI":"10.1109\/LICS.1988.5119"},{"key":"50_CR12","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., XinXin, L.: Equation solving using modal transition systems. In: Proc. 5th LICS, pp. 108\u2013117 (1990)","DOI":"10.1109\/LICS.1990.113738"},{"key":"50_CR13","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: Proc. 19th LICS, pp. 32\u201341 (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"50_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"546","DOI":"10.1007\/978-3-540-24730-2_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Shoham","year":"2004","unstructured":"Shoham, S., Grumberg, O.: Monotonic abstraction-refinement for CTL. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 546\u2013560. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73368-3_50.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T19:00:47Z","timestamp":1737399647000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73368-3_50"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540733676"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73368-3_50","relation":{},"subject":[]}}