{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T15:54:17Z","timestamp":1768319657648,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642221095","type":"print"},{"value":"9783642221101","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-22110-1_26","type":"book-chapter","created":{"date-parts":[[2011,7,4]],"date-time":"2011-07-04T09:08:45Z","timestamp":1309770525000},"page":"333-348","source":"Crossref","is-referenced-by-count":19,"title":["Temporal Property Verification as a Program Analysis Task"],"prefix":"10.1007","author":[{"given":"Byron","family":"Cook","sequence":"first","affiliation":[]},{"given":"Eric","family":"Koskinen","sequence":"additional","affiliation":[]},{"given":"Moshe","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","unstructured":"Cadence SMV, http:\/\/www.kenmcmil.com\/smv.html"},{"key":"26_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, pp. 73\u201385 (2006)","DOI":"10.1145\/1217935.1217943"},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"Berdine, J., Chawdhary, A., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Variance analyses from invariance analyses. In: POPL, pp. 211\u2013224 (2007)","DOI":"10.1145\/1190215.1190249"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/3-540-58179-0_50","volume-title":"Computer Aided Verification","author":"O. Bernholtz","year":"1994","unstructured":"Bernholtz, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking (extended abstract). In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 142\u2013155. Springer, Heidelberg (1994)"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: PLDI, pp. 196\u2013207 (2003)","DOI":"10.1145\/780822.781153"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: The polyranking principle. Automata, Languages and Programming, 1349\u20131361 (2005)","DOI":"10.1007\/11523468_109"},{"issue":"2","key":"26_CR7","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. Burch","year":"1992","unstructured":"Burch, J., Clarke, E., et al.: Symbolic model checking: 1020 states and beyond. Information and computation\u00a098(2), 142\u2013170 (1992)","journal-title":"Information and computation"},{"key":"26_CR8","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL, pp. 289\u2013300 (2009)","DOI":"10.1145\/1594834.1480917"},{"key":"26_CR9","doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E.M., Grumberg, O., Ouaknine, J., Sharygina, N., Touili, T., Veith, H.: State\/event software verification for branching-time specifications. In: IFM (2005), pp. 53\u201369 (2005)","DOI":"10.1007\/11589976_5"},{"key":"26_CR10","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 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)"},{"issue":"2","key":"26_CR11","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1145\/5397.5399","volume":"8","author":"E. Clarke","year":"1986","unstructured":"Clarke, E., Emerson, E., Sistla, A.: Automatic verification of finite-state concurrent systems using temporal logic specifications. TOPLAS\u00a08(2), 263 (1986)","journal-title":"TOPLAS"},{"key":"26_CR12","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model checking (1999)"},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"Clarke, E., Jha, S., Lu, Y., Veith, H.: Tree-like counterexamples in model checking. In: LICS, pp. 19\u201329 (2002)","DOI":"10.1109\/LICS.2002.1029814"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., Vardi, M.Y.: Proving that programs eventually do something good. In: POPL, pp. 265\u2013276 (2007)","DOI":"10.1145\/1190216.1190257"},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"Cook, B., Koskinen, E.: Making prophecies with decision predicates. In: POPL, pp. 399\u2013410 (2011)","DOI":"10.1145\/1926385.1926431"},{"key":"26_CR16","unstructured":"Cook, B., Koskinen, E., Vardi, M.: Branching-time reasoning for programs. Tech. Rep. UCAM-CL-TR-788, University of Cambridge, Computer Laboratory (January 2011), http:\/\/www.cl.cam.ac.uk\/techreports\/UCAM-CL-TR-788.html"},{"key":"26_CR17","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI, pp. 415\u2013426 (2006)","DOI":"10.1145\/1133981.1134029"},{"key":"26_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-49059-0_16","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"G. Delzanno","year":"1999","unstructured":"Delzanno, G., Podelski, A.: Model checking in CLP. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 223\u2013239. Springer, Heidelberg (1999)"},{"key":"26_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61474-5_60","volume-title":"Computer Aided Verification","author":"E. Emerson","year":"1996","unstructured":"Emerson, E., Namjoshi, K.: Automatic verification of parameterized synchronous systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, Springer, Heidelberg (1996)"},{"key":"26_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-642-20551-4_11","volume-title":"Logic-Based Program Synthesis and Transformation","author":"F. Fioravanti","year":"2011","unstructured":"Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Program specialization for verifying infinite state systems: An experimental evaluation. In: Alpuente, M. (ed.) LOPSTR 2010. LNCS, vol.\u00a06564, pp. 164\u2013183. Springer, Heidelberg (2011)"},{"key":"26_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P. Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to b\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 53. Springer, Heidelberg (2001)"},{"key":"26_CR22","unstructured":"Gurfinkel, A.: Personal communication (2010)"},{"key":"26_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/11817963_18","volume-title":"Computer Aided Verification","author":"A. Gurfinkel","year":"2006","unstructured":"Gurfinkel, A., Wei, O., Chechik, M.: yasm: A software model-checker for verification and refutation. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 170\u2013174. Springer, Heidelberg (2006)"},{"key":"26_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/3-540-45657-0_45","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Necula, G.C., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 526. Springer, Heidelberg (2002)"},{"issue":"2","key":"26_CR25","first-page":"312","volume":"47","author":"O. Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J.\u00a0ACM\u00a047(2), 312\u2013360 (2000)","journal-title":"J.\u00a0ACM"},{"key":"26_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/978-3-540-74061-2_26","volume-title":"Static Analysis","author":"S. Magill","year":"2007","unstructured":"Magill, S., Berdine, J., Clarke, E., Cook, B.: Arithmetic strengthening for shape analysis. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 419\u2013436. Springer, Heidelberg (2007)"},{"key":"26_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 123\u2013136. Springer, Heidelberg (2006)"},{"key":"26_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P.W. O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, p. 1. Springer, Heidelberg (2001)"},{"key":"26_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A Complete Method for the Synthesis of Linear Ranking Functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 239\u2013251. Springer, Heidelberg (2004)"},{"key":"26_CR30","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS, pp. 32\u201341 (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"26_CR31","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. In: POPL (2005)","DOI":"10.1145\/1040305.1040317"},{"key":"26_CR32","doi-asserted-by":"crossref","unstructured":"Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: POPL, pp. 49\u201361 (1995)","DOI":"10.1145\/199448.199462"},{"key":"26_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/3-540-49727-7_22","volume-title":"Static Analysis","author":"D.A. Schmidt","year":"1998","unstructured":"Schmidt, D.A., Steffen, B.: Program analysis as model checking of abstract interpretations. In: Levi, G. (ed.) SAS 1998. LNCS, vol.\u00a01503, pp. 351\u2013380. Springer, Heidelberg (1998)"},{"key":"26_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/3-540-61042-1_51","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Stirling","year":"1996","unstructured":"Stirling, C.: Games and modal mu-calculus. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol.\u00a01055, pp. 298\u2013312. Springer, Heidelberg (1996)"},{"key":"26_CR35","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Banff Higher Order Workshop, pp. 238\u2013266 (1995)","DOI":"10.1007\/3-540-60915-6_6"},{"key":"26_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-61474-5_58","volume-title":"Computer Aided Verification","author":"I. Walukiewicz","year":"1996","unstructured":"Walukiewicz, I.: Pushdown processes: Games and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 62\u201374. Springer, Heidelberg (1996)"},{"key":"26_CR37","doi-asserted-by":"crossref","unstructured":"Walukiewicz, I.: Model checking CTL properties of pushdown systems. In: FST TCS, pp. 127\u2013138 (2000)","DOI":"10.1007\/3-540-44450-5_10"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22110-1_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T13:41:14Z","timestamp":1560346874000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22110-1_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642221095","9783642221101"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22110-1_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}