{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:26:50Z","timestamp":1725550010221},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540285847"},{"type":"electronic","value":"9783540319719"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11547662_10","type":"book-chapter","created":{"date-parts":[[2005,9,27]],"date-time":"2005-09-27T14:36:20Z","timestamp":1127831780000},"page":"118-134","source":"Crossref","is-referenced-by-count":4,"title":["Locality-Based Abstractions"],"prefix":"10.1007","author":[{"given":"Javier","family":"Esparza","sequence":"first","affiliation":[]},{"given":"Pierre","family":"Ganty","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Schwoon","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","first-page":"238","volume-title":"Proc. POPL","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. POPL, pp. 238\u2013252. ACM Press, New York (1977)"},{"doi-asserted-by":"crossref","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstraction for model checking C programs. In: Proc. TACAS, pp. 268\u2013283 (2001)","key":"10_CR2","DOI":"10.1007\/3-540-45319-9_19"},{"key":"10_CR3","series-title":"Software Engineering Notes","first-page":"24","volume-title":"Proc. FSE","author":"G. Naumovich","year":"1998","unstructured":"Naumovich, G., Avrunin, G.S.: A conservative data flow algorithm for detecting all pairs of statements that may happen in parallel. In: Proc. FSE. Software Engineering Notes, vol.\u00a023(6), pp. 24\u201334. ACM Press, New York (1998)"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/3-540-48166-4_21","volume-title":"Software Engineering - ESEC\/FSE \u201999","author":"G. Naumovich","year":"1999","unstructured":"Naumovich, G., Avrunin, G.S., Clarke, L.A.: An efficient algorithm for computing mhp information for concurrent Java programs. In: Nierstrasz, O., Lemoine, M. (eds.) ESEC 1999 and ESEC-FSE 1999. LNCS, vol.\u00a01687, pp. 338\u2013354. Springer, Heidelberg (1999)"},{"key":"10_CR5","first-page":"399","volume-title":"Proc. ICSE","author":"G. Naumovich","year":"1999","unstructured":"Naumovich, G., Avrunin, G.S., Clarke, L.A.: Data flow analysis for checking properties of concurrent Java programs. In: Proc. ICSE, pp. 399\u2013410. ACM Press, New York (1999)"},{"doi-asserted-by":"crossref","unstructured":"Kovalyov, A.: Concurrency relations and the safety problem for petri nets. In: ICATPN 1992. LNCS, vol.\u00a0616, pp. 299\u2013309 (1992)","key":"10_CR6","DOI":"10.1007\/3-540-55676-1_17"},{"key":"10_CR7","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/S0004-3702(96)00047-1","volume":"90","author":"A.L. Blum","year":"1997","unstructured":"Blum, A.L., Furst, M.L.: Fast planning through planning graph analysis. Artificial Intelligence\u00a090, 279\u2013298 (1997)","journal-title":"Artificial Intelligence"},{"doi-asserted-by":"crossref","unstructured":"Blum, A.L., Furst, M.L.: Fast planning through planning graph analysis. In: Proc. IJCAI, pp. 1636\u20131642 (1995)","key":"10_CR8","DOI":"10.21236\/ADA303260"},{"key":"10_CR9","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers\u00a035, 677\u2013691 (1986)","journal-title":"IEEE Trans. Computers"},{"doi-asserted-by":"crossref","unstructured":"Srinivasan, A., Kam, T., Malik, S., Brayton, R.K.: Algorithms for discrete function manipulation. In: IEEE\/ACM ICCAD, pp. 92\u201395 (1990)","key":"10_CR10","DOI":"10.1109\/ICCAD.1990.129849"},{"key":"10_CR11","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM\u00a050, 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/3-540-45789-5_29","volume-title":"Static Analysis","author":"F. Ranzato","year":"2002","unstructured":"Ranzato, F., Tapparo, F.: Making abstract model checking strongly preserving. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, pp. 411\u2013427. Springer, Heidelberg (2002)"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/3-540-47764-0_20","volume-title":"Static Analysis","author":"R. Giacobazzi","year":"2001","unstructured":"Giacobazzi, R., Quintarelli, E.: Incompleteness, counterexamples, and refinements in abstract model-checking. In: Cousot, P. (ed.) SAS 2001. LNCS, vol.\u00a02126, pp. 356\u2013373. Springer, Heidelberg (2001)"},{"key":"10_CR14","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1145\/333979.333989","volume":"47","author":"R. Giacobazzi","year":"2000","unstructured":"Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM\u00a047, 361\u2013416 (2000)","journal-title":"J. ACM"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV version 2: An openSource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 359. Springer, Heidelberg (2002)"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/3-540-47813-2_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L.D. Zuck","year":"2002","unstructured":"Zuck, L.D., Pnueli, A., Kesten, Y.: Automatic verification of probabilistic free choice. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol.\u00a02294, pp. 208\u2013224. Springer, Heidelberg (2002)"},{"unstructured":"Heiner, M., Deussen, P.: Petri net based qualitative analysis - a case study. Technical Report I-08\/1995, Brandenburg Tech. Univ., Cottbus (1995)","key":"10_CR17"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11547662_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:57:50Z","timestamp":1619506670000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11547662_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540285847","9783540319719"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/11547662_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}