{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T19:58:21Z","timestamp":1693857501534},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2012,4,27]],"date-time":"2012-04-27T00:00:00Z","timestamp":1335484800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2012,8]]},"DOI":"10.1007\/s10703-012-0153-5","type":"journal-article","created":{"date-parts":[[2012,4,26]],"date-time":"2012-04-26T12:08:44Z","timestamp":1335442124000},"page":"66-82","source":"Crossref","is-referenced-by-count":11,"title":["Temporal property verification as a program analysis task"],"prefix":"10.1007","volume":"41","author":[{"given":"Byron","family":"Cook","sequence":"first","affiliation":[]},{"given":"Eric","family":"Koskinen","sequence":"additional","affiliation":[]},{"given":"Moshe","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,4,27]]},"reference":[{"key":"153_CR1","unstructured":"Cadence SMV, http:\/\/www.kenmcmil.com\/smv.html"},{"key":"153_CR2","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1145\/1218063.1217943","volume":"40","author":"T Ball","year":"2006","unstructured":"Ball T, Bounimova E, Cook B, Levin V, Lichtenberg J, McGarvey C, Ondrusek B, Rajamani SK, Ustuner A (2006) Thorough static analysis of device drivers. SIGOPS Oper Syst Rev 40:73\u201385","journal-title":"SIGOPS Oper Syst Rev"},{"key":"153_CR3","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1145\/1190216.1190249","volume-title":"Proceedings of the 34th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL 2007)","author":"J Berdine","year":"2007","unstructured":"Berdine J, Chawdhary A, Cook B, Distefano D, O\u2019Hearn PW (2007) Variance analyses from invariance analyses. In: Hofmann M, Felleisen M (eds) Proceedings of the 34th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL 2007). ACM, New York, pp 211\u2013224"},{"key":"153_CR4","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/3-540-58179-0_50","volume-title":"Proceedings of the 6th international conference on computer aided verification (CAV \u201994)","author":"O Bernholtz","year":"1994","unstructured":"Bernholtz O, Vardi MY, Wolper P (1994) An automata-theoretic approach to branching-time model checking (extended abstract). In: Dill DL (ed) Proceedings of the 6th international conference on computer aided verification (CAV \u201994). Lecture notes in computer science, vol 818. Springer, Berlin, pp 142\u2013155"},{"issue":"5\u20136","key":"153_CR5","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D Beyer","year":"2007","unstructured":"Beyer D, Henzinger TA, Jhala R, Majumdar R (2007) The software model checker blast. Int J Softw Tools Technol Transf 9(5\u20136):505\u2013525","journal-title":"Int J Softw Tools Technol Transf"},{"key":"153_CR6","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1145\/781131.781153","volume-title":"Proceedings of the ACM SIGPLAN 2003 conference on programming language design and implementation (PLDI\u201903)","author":"B Blanchet","year":"2003","unstructured":"Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Min\u00e9 A, Monniaux D, Rival X (2003) A static analyzer for large safety-critical software. In: Proceedings of the ACM SIGPLAN 2003 conference on programming language design and implementation (PLDI\u201903). ACM, New York, pp 196\u2013207"},{"key":"153_CR7","doi-asserted-by":"crossref","unstructured":"Bradley A, Manna Z, Sipma H (2005) The polyranking principle. Autom Lang Program, 1349\u20131361","DOI":"10.1007\/11523468_109"},{"issue":"2","key":"153_CR8","doi-asserted-by":"crossref","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. (1992) Symbolic model checking: 1020 states and beyond. Inf Comput 98(2):142\u2013170","journal-title":"Inf Comput"},{"key":"153_CR9","first-page":"289","volume-title":"Proceedings of the 36th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL 2009)","author":"C Calcagno","year":"2009","unstructured":"Calcagno C, Distefano D, O\u2019Hearn PW, Yang H (2009) Compositional shape analysis by means of bi-abduction. In: Shao Z, Pierce BC (eds) Proceedings of the 36th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL 2009). ACM, New York, pp 289\u2013300"},{"key":"153_CR10","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/11589976_5","volume-title":"Proceedings of the 5th international conference on integrated formal methods (IFM 2005)","author":"S Chaki","year":"2005","unstructured":"Chaki S, Clarke EM, Grumberg O, Ouaknine J, Sharygina N, Touili T, Veith H (2005) State\/event software verification for branching-time specifications. In: Romijn J, Smith G, van de Pol J (eds) Proceedings of the 5th international conference on integrated formal methods (IFM 2005), vol 3771, pp 53\u201369"},{"key":"153_CR11","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Proceedings of the 14th international conference on computer aided verification (CAV\u201902)","author":"A Cimatti","year":"2002","unstructured":"Cimatti A, Clarke EM, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) Nusmv 2: an opensource tool for symbolic model checking. In: Brinksma E, Larsen KG (eds) Proceedings of the 14th international conference on computer aided verification (CAV\u201902), vol 2404. Springer, Berlin, pp 359\u2013364"},{"key":"153_CR12","unstructured":"Clarke E, Grumberg O, Peled D (1999) Model checking"},{"key":"153_CR13","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1109\/LICS.2002.1029814","volume-title":"Proceedings of the symposium on logic in computer science (LICS\u201902)","author":"E Clarke","year":"2002","unstructured":"Clarke E, Jha S, Lu Y, Veith H (2002) Tree-like counterexamples in model checking. In: Proceedings of the symposium on logic in computer science (LICS\u201902), pp 19\u201329"},{"key":"153_CR14","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst 8:244\u2013263","journal-title":"ACM Trans Program Lang Syst"},{"key":"153_CR15","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1145\/1190216.1190257","volume-title":"Proceedings of the 34th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL 2007)","author":"B Cook","year":"2007","unstructured":"Cook B, Gotsman A, Podelski A, Rybalchenko A, Vardi MY (2007) Proving that programs eventually do something good. In: Proceedings of the 34th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL 2007), pp 265\u2013276"},{"key":"153_CR16","first-page":"399","volume-title":"Proceedings of the 38th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL\u201911)","author":"B Cook","year":"2011","unstructured":"Cook B, Koskinen E (2011) Making prophecies with decision predicates. In: Ball T, Sagiv M (eds) Proceedings of the 38th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL\u201911). ACM, New York, pp 399\u2013410"},{"key":"153_CR17","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/978-3-642-22110-1_26","volume-title":"Proceedings of the 23rd international conference on computer aided verification (CAV\u201911)","author":"B Cook","year":"2011","unstructured":"Cook B, Koskinen E, Vardi MY (2011) Temporal property verification as a program analysis task. In: Gopalakrishnan G, Qadeer S (eds) Proceedings of the 23rd international conference on computer aided verification (CAV\u201911), vol 6806. Springer, Berlin, pp 333\u2013348"},{"key":"153_CR18","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1145\/1133981.1134029","volume-title":"Proceedings of the ACM SIGPLAN 2006 conference on programming language design and implementation","author":"B Cook","year":"2006","unstructured":"Cook B, Podelski A, Rybalchenko A (2006) Termination proofs for systems code. In: Schwartzbach MI, Ball T (eds) Proceedings of the ACM SIGPLAN 2006 conference on programming language design and implementation, Ottawa, Ontario, Canada, June 11\u201314, 2006 ACM, New York, pp 415\u2013426"},{"key":"153_CR19","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/3-540-49059-0_16","volume-title":"Proceedings of the 5th international conference on tools and algorithms for construction and analysis of systems (TACAS \u201999)","author":"G Delzanno","year":"1999","unstructured":"Delzanno G, Podelski A (1999) Model checking in CLP. In: Cleaveland R (ed) Proceedings of the 5th international conference on tools and algorithms for construction and analysis of systems (TACAS \u201999). Lecture notes in computer science, vol 1579. Springer, Berlin, pp 223\u2013239"},{"key":"153_CR20","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/3-540-61474-5_60","volume-title":"Proceedings of the 8th international conference on computer aided verification (CAV \u201996)","author":"EA Emerson","year":"1996","unstructured":"Emerson EA, Namjoshi KS (1996) Automatic verification of parameterized synchronous systems (extended abstract). In: Alur R, Henzinger TA (eds) Proceedings of the 8th international conference on computer aided verification (CAV \u201996), vol 1102. Springer, Berlin, pp 87\u201398"},{"key":"153_CR21","first-page":"164","volume-title":"Proceedings of the 20th international symposium on logic-based program synthesis and transformation (LOPSTR\u201910)","author":"F Fioravanti","year":"2010","unstructured":"Fioravanti F, Pettorossi A, Proietti M, Senni V (2010) Program specialization for verifying infinite state systems: an experimental evaluation. In: Alpuente M (ed) Proceedings of the 20th international symposium on logic-based program synthesis and transformation (LOPSTR\u201910), vol 6564. Springer, Berlin, pp 164\u2013183"},{"key":"153_CR22","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Proceedings of the 13th international conference on computer aided verification (CAV 2001)","author":"P Gastin","year":"2001","unstructured":"Gastin P, Oddoux D (2001) Fast ltl to b\u00fcchi automata translation. In: Berry G, Comon H, Finkel A (eds) Proceedings of the 13th international conference on computer aided verification (CAV 2001), vol 2102. Springer Berlin, pp 53\u201365"},{"key":"153_CR23","unstructured":"Gurfinkel A (2010) Personal communication"},{"key":"153_CR24","doi-asserted-by":"crossref","first-page":"170","DOI":"10.1007\/11817963_18","volume-title":"Proceedings of the 18th international conference on computer aided verification (CAV\u201906)","author":"A Gurfinkel","year":"2006","unstructured":"Gurfinkel A, Wei O, Chechik, M (2006) Yasm: a software model-checker for verification and refutation. In: Ball T, Jones RB (eds) Proceedings of the 18th international conference on computer aided verification (CAV\u201906), vol 4144, pp 170\u2013174"},{"key":"153_CR25","unstructured":"Koskinen E (2012) Temporal verification of programs. PhD thesis, University of Cambridge. To appear"},{"issue":"2","key":"153_CR26","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O Kupferman","year":"2000","unstructured":"Kupferman O, Vardi M, Wolper P (2000) An automata-theoretic approach to branching-time model checking. J ACM 47(2):312\u2013360","journal-title":"J ACM"},{"key":"153_CR27","first-page":"419","volume-title":"Proceedings of the 14th international static analysis symposium (SAS 2007)","author":"S Magill","year":"2007","unstructured":"Magill S, Berdine J, Clarke EM, Cook B (2007) Arithmetic strengthening for shape analysis. In: Nielson HR, Fil\u00e9 G (eds) Proceedings of the 14th international static analysis symposium (SAS 2007), vol 4634. Springer, Berlin, pp 419\u2013436"},{"key":"153_CR28","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer science logic","author":"P O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn P, Reynolds J, Yang H (2001) Local reasoning about programs that alter data structures. In: Computer science logic, pp 1\u201319"},{"key":"153_CR29","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Proceedings of the 5th international conference on verification, model checking, and abstract interpretation (VMCAI\u201904)","author":"A Podelski","year":"2004","unstructured":"Podelski A, Rybalchenko A (2004) A complete method for the synthesis of linear ranking functions. In: Steffen B, Levi G (eds) Proceedings of the 5th international conference on verification, model checking, and abstract interpretation (VMCAI\u201904), vol 2937. Springer, Berlin, pp 239\u2013251"},{"key":"153_CR30","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1109\/LICS.2004.1319598","volume-title":"Proceedings of the 19th IEEE symposium on logic in computer science (LICS 2004)","author":"A Podelski","year":"2004","unstructured":"Podelski A, Rybalchenko A (2004) Transition invariants. In: Proceedings of the 19th IEEE symposium on logic in computer science (LICS 2004). IEEE Computer Society, New York, pp 32\u201341"},{"key":"153_CR31","volume-title":"Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL 2005)","author":"A Podelski","year":"2005","unstructured":"Podelski A, Rybalchenko A (2005) Transition predicate abstraction and fair termination. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL 2005)"},{"key":"153_CR32","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1145\/199448.199462","volume-title":"Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL\u201995)","author":"T Reps","year":"1995","unstructured":"Reps T, Horwitz S, Sagiv M (1995) Precise interprocedural dataflow analysis via graph reachability. In: Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL\u201995), pp 49\u201361"},{"key":"153_CR33","first-page":"351","volume-title":"Proceedings of the 5th international static analysis symposium (SAS \u201998)","author":"DA Schmidt","year":"1998","unstructured":"Schmidt DA, Steffen B (1998) Program analysis as model checking of abstract interpretations. In: Levi G (ed) Proceedings of the 5th international static analysis symposium (SAS \u201998), vol 1503. Springer, Berlin, pp 351\u2013380"},{"key":"153_CR34","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/3-540-61042-1_51","volume-title":"Proceedings of the second international workshop on tools and algorithms for construction and analysis of systems (TACAS \u201996)","author":"C Stirling","year":"1996","unstructured":"Stirling C (1996) Games and modal mu-calculus. In: Margaria T, Steffen B (eds) Proceedings of the second international workshop on tools and algorithms for construction and analysis of systems (TACAS \u201996), vol 1055, pp 298\u2013312"},{"key":"153_CR35","first-page":"238","volume-title":"Banff Higher order workshop","author":"MY Vardi","year":"1995","unstructured":"Vardi MY (1995) An automata-theoretic approach to linear temporal logic. In: Banff Higher order workshop, pp 238\u2013266"},{"key":"153_CR36","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/3-540-61474-5_58","volume-title":"Proceedings of the 8th international conference on computer aided verification","author":"I Walukiewicz","year":"1996","unstructured":"Walukiewicz I (1996) Pushdown processes: games and model checking. In: Alur R, Henzinger TA (eds) Proceedings of the 8th international conference on computer aided verification. Lecture notes in computer science, vol 1102. Springer, Berlin, pp 62\u201374"},{"key":"153_CR37","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/3-540-44450-5_10","volume-title":"Proceedings of the 20th conference on foundations of software technology and theoretical computer science (FST TCS 2000)","author":"I Walukiewicz","year":"2000","unstructured":"Walukiewicz I (2000) Model checking CTL properties of pushdown systems. In: Kapoor S, Prasad S (eds) Proceedings of the 20th conference on foundations of software technology and theoretical computer science (FST TCS 2000). Springer, Berlin, pp 127\u2013138. 1974"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0153-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-012-0153-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0153-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,28]],"date-time":"2019-06-28T00:06:26Z","timestamp":1561680386000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-012-0153-5"}},"subtitle":["Extended Version"],"short-title":[],"issued":{"date-parts":[[2012,4,27]]},"references-count":37,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["153"],"URL":"https:\/\/doi.org\/10.1007\/s10703-012-0153-5","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,4,27]]}}}