{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:00:11Z","timestamp":1725494411819},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540697350"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-69738-1_13","type":"book-chapter","created":{"date-parts":[[2007,11,12]],"date-time":"2007-11-12T07:58:07Z","timestamp":1194854287000},"page":"182-198","source":"Crossref","is-referenced-by-count":15,"title":["The Spotlight Principle"],"prefix":"10.1007","author":[{"given":"Bj\u00f6rn","family":"Wachter","sequence":"first","affiliation":[]},{"given":"Bernd","family":"Westphal","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Hsu, A., Eskafi, F., Sachs, S., Varaiya, P.: The Design of Platoon Maneuver Protocols for IVHS. PATH Research Report UCB-ITS-PRR-91-6, Institute of Transportation Studies, University of California at Berkeley (1991)","key":"13_CR1","DOI":"10.23919\/ACC.1991.4791861"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","first-page":"107","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"2003","unstructured":"Pnueli, A., Xu, J., Zuck, L.: Liveness with (0,1,infty)-counter abstraction. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 107\u2013133. Springer, Heidelberg (2003)"},{"key":"13_CR3","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/BF00289237","volume":"21","author":"B.D. Lubachevsky","year":"1984","unstructured":"Lubachevsky, B.D.: An Approach to Automating the Verification of Compact Parallel Coordination Programs. Acta Informatica\u00a021, 125\u2013169 (1984)","journal-title":"Acta Informatica"},{"key":"13_CR4","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1145\/285055.285057","volume":"45","author":"F. Pong","year":"1998","unstructured":"Pong, F., Dubois, M.: Formal verification of complex coherence protocols using symbolic state models. J. ACM\u00a045, 557\u2013587 (1998)","journal-title":"J. ACM"},{"key":"13_CR5","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S.M. German","year":"1992","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM\u00a039, 675\u2013735 (1992)","journal-title":"J. ACM"},{"key":"13_CR6","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":"2005","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 (2005)"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/3-540-48153-2_17","volume-title":"Correct Hardware Design and Verification Methods","author":"K.L. McMillan","year":"1999","unstructured":"McMillan, K.L.: Verification of infinite state systems by compositional model checking (charme). In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 219\u2013234. Springer, Heidelberg (1999)"},{"doi-asserted-by":"crossref","unstructured":"Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems 22 (2001)","key":"13_CR8","DOI":"10.1145\/514188.514190"},{"key":"13_CR9","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1145\/373243.360206","volume":"36","author":"E. Yahav","year":"2001","unstructured":"Yahav, E.: Verifying safety properties of concurrent Java programs using 3-valued logic. ACM SIGPLAN Notices\u00a036, 27\u201340 (2001)","journal-title":"ACM SIGPLAN Notices"},{"key":"13_CR10","first-page":"25","volume-title":"Proceedings of the ACM SIGPLAN conference on Programming language design and implementation","author":"E. Yahav","year":"2004","unstructured":"Yahav, E., Ramalingam, G.: Verifying safety properties using separation and heterogeneous abstractions. In: Proceedings of the ACM SIGPLAN conference on Programming language design and implementation, pp. 25\u201334. ACM Press, New York (2004)"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/3-540-36575-3_15","volume-title":"Programming Languages and Systems","author":"E. Yahav","year":"2003","unstructured":"Yahav, E., et al.: Verifying Temporal Heap Properties Specified via Evolution Logic. In: Degano, P. (ed.) ESOP 2003 and ETAPS 2003. LNCS, vol.\u00a02618, pp. 204\u2013222. Springer, Heidelberg (2003)"},{"doi-asserted-by":"crossref","unstructured":"Distefano, D., Katoen, J.P., Rensink, A.: Who is Pointing When to Whom? In: Proceedings of the 24th International Conference On Foundations of Software Technology and Theoretical Computer Science, pp. 250\u2013262 (2004)","key":"13_CR12","DOI":"10.1007\/978-3-540-30538-5_21"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/10722167_25","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2000","unstructured":"McMillan, K.L., Qadeer, S., Saxe, J.B.: Induction in Compositional Model Checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 15\u201319. Springer, Heidelberg (2000)"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1007\/978-3-540-30579-8_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R. Manevich","year":"2005","unstructured":"Manevich, R., et al.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 181\u2013198. Springer, Heidelberg (2005)"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1007\/978-3-540-39656-7_4","volume-title":"Formal Methods for Components and Objects","author":"W. Damm","year":"2003","unstructured":"Damm, W., Westphal, B.: Live and Let Die: LSC-based Verification of UML-Models. In: de Boer, F.S., et al. (eds.) FMCO 2002. LNCS, vol.\u00a02852, pp. 99\u2013135. Springer, Heidelberg (2003)"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","first-page":"310","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Dams","year":"2002","unstructured":"Dams, D., Namjoshi, K.S.: Shape Analysis through Predicate Abstraction and Model Checking. In: Zuck, L.D., et al. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 310\u2013324. Springer, Heidelberg (2002)"},{"key":"13_CR17","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/s100090050040","volume":"2","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Control and Data Abstraction: The Cornerstones of Practical Formal Verification. International Journal on Software Tools for Technology Transfer\u00a02, 328\u2013342 (2000)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"13_CR18","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L. Lamport","year":"1974","unstructured":"Lamport, L.: A New Solution of Dijkstra\u2019s Concurrent Programming Problem. Communications of the ACM\u00a017, 453\u2013455 (1974)","journal-title":"Communications of the ACM"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1007\/978-3-540-45099-3_15","volume-title":"Static Analysis","author":"T. Lev-Ami","year":"2000","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: A System for Implementing Static Analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, pp. 280\u2013301. Springer, Heidelberg (2000)"},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/11547662_19","volume-title":"Static Analysis","author":"A. Podelski","year":"2005","unstructured":"Podelski, A., Wies, T.: Boolean Heaps. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 268\u2013283. Springer, Heidelberg (2005)"},{"unstructured":"Wachter, B.: Checking universally quantified temporal properties with three- valued analysis. Master\u2019s thesis, Universit\u00e4t des Saarlandes (2005)","key":"13_CR21"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69738-1_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T00:45:03Z","timestamp":1620002703000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69738-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540697350"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69738-1_13","relation":{},"subject":[]}}