{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:59:09Z","timestamp":1725551949876},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540311393"},{"type":"electronic","value":"9783540316220"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11609773_22","type":"book-chapter","created":{"date-parts":[[2005,12,12]],"date-time":"2005-12-12T07:28:57Z","timestamp":1134372537000},"page":"332-347","source":"Crossref","is-referenced-by-count":5,"title":["Strong Preservation of Temporal Fixpoint-Based Operators by Abstract Interpretation"],"prefix":"10.1007","author":[{"given":"Francesco","family":"Ranzato","sequence":"first","affiliation":[]},{"given":"Francesco","family":"Tapparo","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/3-540-44577-3_12","volume-title":"Informatics","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Progress on the state explosion problem in model checking. In: Wilhelm, R. (ed.) Informatics: 10 Years Back, 10 Years Ahead. LNCS, vol.\u00a02000, pp. 176\u2013194. Springer, Heidelberg (2001)"},{"issue":"5","key":"22_CR2","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.: Model checking and abstraction. ACM Trans. Program. Lang. Syst.\u00a016(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"22_CR3","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"22_CR4","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: Proc. 4\n                  \n                    \n                  \n                  $^{\\mathit{th}}$\n                 ACM POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. 6\n                  \n                    \n                  \n                  $^{\\mathit{th}}$\n                 ACM POPL, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"issue":"1","key":"22_CR6","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1023\/A:1008649901864","volume":"6","author":"P. Cousot","year":"1999","unstructured":"Cousot, P., Cousot, R.: Refining model checking by abstract interpretation. Automated Software Engineering Journal\u00a06(1), 69\u201395 (1999)","journal-title":"Automated Software Engineering Journal"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Temporal abstract interpretation. In: Proc. 27\n                  \n                    \n                  \n                  $^{\\mathit{th}}$\n                 ACM POPL, pp. 12\u201325 (2000)","DOI":"10.1145\/325694.325699"},{"key":"22_CR8","unstructured":"Dams, D.: Abstract Interpretation and Partition Refinement for Model Checking. PhD Thesis, Eindhoven Univ (1996)"},{"issue":"1","key":"22_CR9","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1093\/jigpal\/7.1.55","volume":"7","author":"D. Dams","year":"1999","unstructured":"Dams, D.: Flat fragments of CTL and CTL*: separating the expressive and distinguishing powers. Logic J. of the IGPL\u00a07(1), 55\u201378 (1999)","journal-title":"Logic J. of the IGPL"},{"issue":"5","key":"22_CR10","first-page":"1512","volume":"16","author":"D. Dams","year":"1997","unstructured":"Dams, D., Grumberg, O., Gerth, R.: Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst.\u00a016(5), 1512\u20131542 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/3-540-47764-0_20","volume-title":"Static Analysis","author":"R. Giacobazzi","year":"2001","unstructured":"Giacobazzi, R., Quintarelli, E.: Incompleteness, counterexamples and refinements in abstract model checking. In: Cousot, P. (ed.) SAS 2001. LNCS, vol.\u00a02126, pp. 356\u2013373. Springer, Heidelberg (2001)"},{"issue":"2","key":"22_CR12","first-page":"361","volume":"47","author":"R. Giacobazzi","year":"2000","unstructured":"Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J.\u00a0ACM\u00a047(2), 361\u2013416 (2000)","journal-title":"J.\u00a0ACM"},{"issue":"3","key":"22_CR13","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Trans. Program. Lang. Syst.\u00a016(3), 843\u2013871 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: Proc. 36\n                  \n                    \n                  \n                  $^{\\mathit{th}}$\n                 FOCS, pp. 453\u2013462 (1995)","DOI":"10.1109\/SFCS.1995.492576"},{"key":"22_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design\u00a06, 1\u201336 (1995)","journal-title":"Formal Methods in System Design"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/3-540-45789-5_30","volume-title":"Static Analysis","author":"D. Mass\u00e9","year":"2002","unstructured":"Mass\u00e9, D.: Semantics for abstract interpretation-based static analyzes of temporal properties. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, pp. 428\u2013443. Springer, Heidelberg (2002)"},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-540-24725-8_3","volume-title":"Programming Languages and Systems","author":"F. Ranzato","year":"2004","unstructured":"Ranzato, F., Tapparo, F.: Strong preservation as completeness in abstract interpretation. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 18\u201332. Springer, Heidelberg (2004)"},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-540-31980-1_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F. Ranzato","year":"2005","unstructured":"Ranzato, F., Tapparo, F.: An abstract interpretation-based refinement algorithm for strong preservation. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 140\u2013156. Springer, Heidelberg (2005)"},{"key":"22_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-540-27864-1_5","volume-title":"Static Analysis","author":"D.A. Schmidt","year":"2004","unstructured":"Schmidt, D.A.: Closed and logical relations for over- and under-approximation of powersets. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 22\u201337. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11609773_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:07:02Z","timestamp":1619507222000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11609773_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540311393","9783540316220"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/11609773_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}