{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:47:06Z","timestamp":1725540426941},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642050886"},{"type":"electronic","value":"9783642050893"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-05089-3_8","type":"book-chapter","created":{"date-parts":[[2009,11,3]],"date-time":"2009-11-03T22:31:40Z","timestamp":1257287500000},"page":"106-122","source":"Crossref","is-referenced-by-count":13,"title":["Three-Valued Spotlight Abstractions"],"prefix":"10.1007","author":[{"given":"Jonas","family":"Schrieb","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Wonisch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","volume-title":"Model checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model checking. MIT Press, Cambridge (1999)"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)","DOI":"10.1145\/512950.512973"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. In: 19th ACM POPL (1992)","DOI":"10.1145\/143165.143235"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The Software Model Checker Blast: Applications to Software Engineering. In: STTT (2007)","DOI":"10.1007\/s10009-007-0044-z"},{"key":"8_CR5","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., Cook, B., Levin, V., Rajamani, S.K.: 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)"},{"issue":"6","key":"8_CR6","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1109\/TSE.2004.22","volume":"30","author":"S. Chaki","year":"2004","unstructured":"Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular Verification of Software Components in C. IEEE Trans. on Software Engineering (TSE)\u00a030(6), 388\u2013402 (2004)","journal-title":"IEEE Trans. on Software Engineering (TSE)"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-69611-7_16","volume-title":"Practical Aspects of Declarative Languages","author":"A. Podelski","year":"2007","unstructured":"Podelski, A., Rybalchenko, A.: ARMC: The logical choice for software model checking with abstraction refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol.\u00a04354, pp. 245\u2013259. Springer, Heidelberg (2007)"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.\u00a03440, pp. 570\u2013574. Springer, Heidelberg (2005)"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/3-540-45657-0_9","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"2002","unstructured":"Pnueli, A., Xu, J., Zuck, L.D.: Liveness with (0, 1, infty)-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 107\u2013122. Springer, Heidelberg (2002)"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/11609773_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E.M. Clarke","year":"2006","unstructured":"Clarke, E.M., Talupur, M., Veith, H.: Environment abstraction for parameterized verification. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 126\u2013141. Springer, Heidelberg (2006)"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-540-69738-1_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B. Wachter","year":"2007","unstructured":"Wachter, B., Westphal, B.: The Spotlight Principle: On Process-Summarizing State Abstractions. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 182\u2013198. Springer, Heidelberg (2007)"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: Symposium on Principles of Programming Languages, pp. 105\u2013118 (1999)","DOI":"10.1145\/292540.292552"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1007\/978-3-540-27836-8_26","volume-title":"Automata, Languages and Programming","author":"G. Bruns","year":"2004","unstructured":"Bruns, G., Godefroid, P.: Model checking with multi-valued logics. In: D\u00edaz, J., Karhum\u00e4ki, J., Lepist\u00f6, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol.\u00a03142, pp. 281\u2013293. Springer, Heidelberg (2004)"},{"issue":"4","key":"8_CR14","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1145\/990010.990011","volume":"12","author":"M. Chechik","year":"2003","unstructured":"Chechik, M., Devereux, B., Easterbrook, S.M., Gurfinkel, A.: Multi-valued symbolic model-checking. ACM Trans. Softw. Eng. Methodol.\u00a012(4), 371\u2013408 (2003)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/11691372_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Gurfinkel","year":"2006","unstructured":"Gurfinkel, A., Chechik, M.: Why waste a perfectly good abstraction? In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 212\u2013226. Springer, Heidelberg (2006)"},{"key":"8_CR16","first-page":"804","volume-title":"ICSE","author":"S.M. Easterbrook","year":"2003","unstructured":"Easterbrook, S.M., Chechik, M., Devereux, B., et al.: \u03c7chek: A model checker for multi-valued reasoning. In: ICSE, pp. 804\u2013805. IEEE Computer Society, Los Alamitos (2003)"},{"key":"8_CR17","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":"8_CR18","doi-asserted-by":"crossref","first-page":"113","DOI":"10.3233\/FI-1994-201234","volume":"20","author":"M. Fitting","year":"1994","unstructured":"Fitting, M.: Kleene\u2019s three valued logics and their children. FI\u00a020, 113\u2013131 (1994)","journal-title":"FI"},{"key":"8_CR19","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM TPLS\u00a08, 244\u2013263 (1986)","journal-title":"ACM TPLS"},{"issue":"1","key":"8_CR20","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/s10009-002-0095-0","volume":"5","author":"T. Ball","year":"2003","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstraction for model checking C programs. STTT\u00a05(1), 49\u201358 (2003)","journal-title":"STTT"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Schrieb, J., Wehrheim, H., Wonisch, D.: Three-valued spotlight abstractions (2009), http:\/\/www.cs.upb.de\/en\/ag-bloemer\/people\/jonas","DOI":"10.1007\/978-3-642-05089-3_8"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1007\/978-3-540-45236-2_28","volume-title":"FME 2003: Formal Methods","author":"A. Gurfinkel","year":"2003","unstructured":"Gurfinkel, A., Chechik, M.: Generating counterexamples for multi-valued model-checking. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 503\u2013521. Springer, Heidelberg (2003)"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"262","DOI":"10.1007\/978-3-540-45069-6_27","volume-title":"Computer Aided Verification","author":"T. Henzinger","year":"2003","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., Qadeer, S.: Thread-modular abstraction refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 262\u2013274. Springer, Heidelberg (2003)"},{"issue":"9","key":"8_CR24","doi-asserted-by":"publisher","first-page":"569","DOI":"10.1145\/365559.365617","volume":"8","author":"E.W. Dijkstra","year":"1965","unstructured":"Dijkstra, E.W.: Solution of a problem in concurrent programming control. Commun. ACM\u00a08(9), 569 (1965)","journal-title":"Commun. ACM"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-68855-6_2","volume-title":"Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2008","author":"T. Toben","year":"2008","unstructured":"Toben, T.: Counterexample guided spotlight abstraction refinement. In: Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds.) FORTE 2008. LNCS, vol.\u00a05048, pp. 21\u201336. Springer, Heidelberg (2008)"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58\u201370 (2002)","DOI":"10.1145\/503272.503279"},{"key":"8_CR27","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1145\/996841.996846","volume-title":"PLDI","author":"E. Yahav","year":"2004","unstructured":"Yahav, E., Ramalingam, G.: Verifying safety properties using separation and heterogeneous abstractions. In: PLDI, pp. 25\u201334. ACM, New York (2004)"}],"container-title":["Lecture Notes in Computer Science","FM 2009: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-05089-3_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:47:42Z","timestamp":1606186062000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-05089-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642050886","9783642050893"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-05089-3_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}