{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T14:17:14Z","timestamp":1778249834643,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540003489","type":"print"},{"value":"9783540363842","type":"electronic"}],"license":[{"start":{"date-parts":[[2002,12,16]],"date-time":"2002-12-16T00:00:00Z","timestamp":1039996800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,12,16]],"date-time":"2002-12-16T00:00:00Z","timestamp":1039996800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36384-x_16","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T09:21:13Z","timestamp":1196328073000},"page":"174-188","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Lifting Temporal Proofs through Abstractions"],"prefix":"10.1007","author":[{"given":"Kedar S.","family":"Namjoshi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,12,16]]},"reference":[{"key":"16_CR1","series-title":"Lect Notes Comput Sci","volume-title":"CAV","author":"T. Arons","year":"2001","unstructured":"T. Arons, A. Pnueli, S. Ruah, J. Xu, and L. D. Zuck. Parameterized verification with automatically computed inductive assertions. In CAV, volume 2102 of LNCS, 2001."},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"M. Browne, E.M. Clarke, and O. Grumberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59, 1988.","DOI":"10.21236\/ADA188620"},{"key":"16_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Design and synthesis of synchronization skeletons using branching time temporal logic","author":"E.M. Clarke","year":"1981","unstructured":"E.M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Workshop on Logics of Programs, volume 131 of LNCS. Springer-Verlag, 1981."},{"key":"16_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0028174","volume-title":"CAV","author":"E. M. Clarke","year":"1993","unstructured":"E. M. Clarke, T. Filkorn, and S. Jha. Exploiting symmetry in temporal logic model checking. In CAV, volume 697 of LNCS, 1993."},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"E.W. Dijkstra and C.S. Scholten. Predicate Calculus and Program Semantics. Springer Verlag, 1990.","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"16_CR6","unstructured":"E.A. Emerson and C.S. Jutla. Tree automata, mu-calculus and determinacy (extended abstract). In FOCS, 1991."},{"key":"16_CR7","unstructured":"E.A. and C-L. Lei. Efficient model checking in fragments of the propositional mu-calculus (extended abstract). In LICS, 1986."},{"key":"16_CR8","series-title":"Lect Notes Comput Sci","volume-title":"CAV","author":"E. A. Emerson","year":"1993","unstructured":"E. A. Emerson and A. P. Sistla. Symmetry and model checking. In CAV, volume 697 of LNCS, 1993."},{"key":"16_CR9","series-title":"Lect Notes Comput Sci","volume-title":"CAV","author":"S. Graf","year":"1997","unstructured":"S. Graf and H. Sa\u00efdi. Construction of abstract state graphs with PVS. In CAV, volume 1254 of LNCS, 1997."},{"key":"16_CR10","series-title":"Lect Notes Comput Sci","volume-title":"CAV","author":"R.H. Hardin","year":"1996","unstructured":"R.H. Hardin, Z. Har\u2019el, and R.P. Kurshan. COSPAN. In CAV, volume 1102 of LNCS, 1996."},{"key":"16_CR11","series-title":"Lect Notes Comput Sci","volume-title":"CAV","author":"T. A. Henzinger","year":"2002","unstructured":"T. A. Henzinger, R. Jhala, R. Majumdar, G. C. Necula, G. Sutre, and W. Weimer. Temporal-safety proofs for systems code. In CAV, volume 2404 of LNCS, 2002."},{"key":"16_CR12","series-title":"Lect Notes Comput Sci","volume-title":"ESOP","author":"M. Huth","year":"2001","unstructured":"M. Huth, R. Jagadeesan, and D. Schmidt. Modal transition systems: a foundation for three-valued program analysis. In ESOP, number 2028 in LNCS, 2001."},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"M. Hennessy and R. Milner. Algebriac laws for nondeterminism and concurrency. J.ACM, 1985.","DOI":"10.1145\/2455.2460"},{"key":"16_CR14","series-title":"Lect Notes Comput Sci","volume-title":"MFCS","author":"D. Janin","year":"1995","unstructured":"D. Janin and I. Walukiewicz. Automata for the modal mu-calulus and related results. In MFCS, volume 969 of LNCS, 1995."},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"R.M. Keller. Formal verification of parallel programs. CACM, 1976.","DOI":"10.1145\/360248.360251"},{"key":"16_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0025769","volume-title":"ICALP","author":"D. Kozen","year":"1982","unstructured":"D. Kozen. Results on the propositional mu-calculus. In ICALP, volume 140 of LNCS, 1982."},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Y. Kesten and A. Pnueli. Verification by augmented finitary abstraction. Information and Computation, 163(1), 2000.","DOI":"10.1006\/inco.2000.3000"},{"key":"16_CR18","unstructured":"K.G. Larsen and B. Thomsen. A modal process logic. In LICS, 1988."},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"16_CR20","unstructured":"E. Mendelson. Introduction to Mathematical Logic. Chapman and Hall (4th Edition), 1997."},{"key":"16_CR21","unstructured":"R. Milner. An algebraic definition of simulation between programs. In 2nd IJCAI, 1971."},{"key":"16_CR22","series-title":"Lect Notes Comput Sci","volume-title":"CAV","author":"K. S. Namjoshi","year":"2001","unstructured":"K. S. Namjoshi. Certifying model checkers. In CAV, volume 2102 of LNCS, 2001."},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"G.C. Necula and P. Lee. Safe kernel extensions without run-time checking. In OSDI, 1996.","DOI":"10.1145\/238721.238781"},{"key":"16_CR24","series-title":"Lect Notes Comput Sci","volume-title":"Concurrency and automata on infinite sequences","author":"D. Park","year":"1981","unstructured":"D. Park. Concurrency and automata on infinite sequences, volume 154 of LNCS. Springer Verlag, 1981."},{"key":"16_CR25","series-title":"Lect Notes Comput Sci","volume-title":"FSTTCS","author":"D. Peled","year":"2001","unstructured":"D. Peled, A. Pnueli, and L. D. Zuck. From falsification to verification. In FSTTCS, volume 2245 of LNCS, 2001."},{"key":"16_CR26","unstructured":"W. Pugh. The Omega test: a fast and practical integer programming algorithm for dependence analysis. CACM, 35(8), 1992. web page: http:\/\/www.cs.umd.edu\/projects\/omega\/omega.html."},{"key":"16_CR27","series-title":"Lect Notes Comput Sci","volume-title":"Specification and verification of concurrent systems in CESAR","author":"J.P. Queille","year":"1982","unstructured":"J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proc. of the 5th International Symposium on Programming, volume 137 of LNCS, 1982."},{"key":"16_CR28","doi-asserted-by":"crossref","unstructured":"A. Roychoudhury, C.R. Ramakrishnan, and I.V. Ramakrishnan. Justifying proofs using memo tables. In PPDP, 2000.","DOI":"10.1145\/351268.351290"},{"key":"16_CR29","doi-asserted-by":"crossref","unstructured":"R. Sekar, C. R. Ramakrishnan, I. V. Ramakrishnan, and S. A. Smolka. Model-carrying code (MCC): A new paradigm for mobile-code security. In New Security Paradigms Workshop, 2002.","DOI":"10.1145\/508172.508175"},{"key":"16_CR30","series-title":"Lect Notes Comput Sci","volume-title":"Modal and temporal logics for processes","author":"C. Stirling","year":"1995","unstructured":"C. Stirling. Modal and temporal logics for processes. In Ban. Higher Order Workshop, volume 1043 of LNCS. Springer Verlag, 1995."},{"key":"16_CR31","series-title":"Lect Notes Comput Sci","volume-title":"CAV","author":"L. Tan","year":"2002","unstructured":"L. Tan and R. Cleaveland. Evidence-based model checking. In CAV, volume 2404 of LNCS, 2002."},{"key":"16_CR32","doi-asserted-by":"crossref","unstructured":"P. Wolper. Expressing interesting properties of programs in propositional temporal logic. In POPL, 1986.","DOI":"10.1145\/512644.512661"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36384-X_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T13:56:41Z","timestamp":1778248601000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-36384-X_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,12,16]]},"ISBN":["9783540003489","9783540363842"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/3-540-36384-x_16","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002,12,16]]},"assertion":[{"value":"16 December 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}