{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:00:40Z","timestamp":1770274840957,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540423140","type":"print"},{"value":"9783540477648","type":"electronic"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-47764-0_20","type":"book-chapter","created":{"date-parts":[[2007,6,12]],"date-time":"2007-06-12T00:55:55Z","timestamp":1181609755000},"page":"356-373","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":63,"title":["Incompleteness, Counterexamples, and Refinements in Abstract Model-Checking"],"prefix":"10.1007","author":[{"given":"Roberto","family":"Giacobazzi","sequence":"first","affiliation":[]},{"given":"Elisa","family":"Quintarelli","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,7,4]]},"reference":[{"issue":"2","key":"20_CR1","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent system using temporal logic specification. ACM Trans. Program. Lang. Syst., 8(2):244\u2013263, 1986.","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"20_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Proc. of the 12th Internat. Conf. on Computer Aided Verification (CAV\u2019 00)","author":"E. M. Clarke","year":"2000","unstructured":"E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Proc. of the 12th Internat. Conf. on Computer Aided Verification (CAV\u2019 00), volume 1855 of Lecture Notes in Computer Science, pages 154\u2013169. Springer-Verlag, Berlin, 2000."},{"issue":"5","key":"20_CR3","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. M. Clarke","year":"1994","unstructured":"E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. ACM Trans. Program. Lang. Syst., 16(5):1512\u20131542, 1994.","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"20_CR4","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1145\/263699.263744","volume-title":"Conference Record of the 24th ACM Symp. on Principles of Programming Languages (POPL\u2019 97)","author":"P. Cousot","year":"1997","unstructured":"P. Cousot. Types as abstract interpretations (Invited Paper). In Conference Record of the 24th ACM Symp. on Principles of Programming Languages (POPL\u2019 97), pages 316\u2013331. ACM Press, New York, 1997."},{"key":"20_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44914-0_1","volume-title":"Proceedings of the Fourth International Symposium on Abstraction, Reformulations and Approximation, SARA\u20192000","author":"P. Cousot","year":"2000","unstructured":"P. Cousot. Partial completeness of abstract fixpoint checking, invited paper. In Proceedings of the Fourth International Symposium on Abstraction, Reformulations and Approximation, SARA\u20192000, Lecture Notes in Artificial Intelligence 1864, pages 1\u201325, Horseshoe Bay, Texas, USA, 26\u201329 July 2000. Springer-Verlag, Berlin, Germany."},{"key":"20_CR6","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1145\/512950.512973","volume-title":"Conference Record of the 4th ACM Symp. on Principles of Programming Languages (POPL\u2019 77)","author":"P. Cousot","year":"1977","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th ACM Symp. on Principles of Programming Languages (POPL\u2019 77), pages 238\u2013252. ACM Press, New York, 1977."},{"key":"20_CR7","first-page":"269","volume-title":"Conference Record of the 6th ACM Symp. on Principles of Programming Languages (POPL\u201979)","author":"P. Cousot","year":"1979","unstructured":"P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Conference Record of the 6th ACM Symp. on Principles of Programming Languages (POPL\u201979), pages 269\u2013282. ACM Press, New York, 1979."},{"issue":"1","key":"20_CR8","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1023\/A:1008649901864","volume":"6","author":"P. Cousot","year":"1999","unstructured":"P. Cousot and R. Cousot. Refining model checking by abstract interpretation. Automated Software Engineering, 6(1):69\u201395, 1999.","journal-title":"Automated Software Engineering"},{"key":"20_CR9","first-page":"12","volume-title":"Conference Record of the Twentyseventh Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"P. Cousot","year":"2000","unstructured":"P. Cousot and R. Cousot. Temporal abstract interpretation. In Conference Record of the Twentyseventh Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 12\u201325, Boston, Mass., January 2000. ACM Press, New York,NY."},{"issue":"2","key":"20_CR10","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"D. Dams","year":"1997","unstructured":"D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst., 19(2):253\u2013291, 1997.","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"20_CR11","series-title":"Formal Models and Semantics","volume-title":"Handbook of Theoretical Computer Science","author":"E. A. Emerson","year":"1990","unstructured":"E. A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics. Elsevier, Amsterdam and The MIT Press, Cambridge, Mass., 1990."},{"issue":"2","key":"20_CR12","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1145\/234528.234742","volume":"28","author":"G. Fil\u00e9","year":"1996","unstructured":"G. Fil\u00e9, R. Giacobazzi, and F. Ranzato. A unifying view of abstract domain design. A CM Comput. Surv., 28(2):333\u2013336, 1996.","journal-title":"A CM Comput. Surv."},{"key":"20_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"771","DOI":"10.1007\/3-540-63165-8_230","volume-title":"Proc. of the 24th Internat. Colloq. on Automata, Languages and Programming (ICALP\u2019 97)","author":"R. Giacobazzi","year":"1997","unstructured":"R. Giacobazzi and F. Ranzato. Refining and compressing abstract domains. In P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela, editors, Proc. of the 24th Internat. Colloq. on Automata, Languages and Programming (ICALP\u2019 97), volume 1256 of Lecture Notes in Computer Science, pages 771\u2013781. Springer-Verlag, Berlin, 1997."},{"issue":"2","key":"20_CR14","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1145\/333979.333989","volume":"47","author":"R. Giacobazzi","year":"2000","unstructured":"R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract interpretation complete. Journal of the ACM, 47(2):361\u2013416, March 2000.","journal-title":"Journal of the ACM"},{"key":"20_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods Syst. Des., 6:1\u201336, 1995.","journal-title":"Formal Methods Syst. Des."},{"key":"20_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z. Manna","year":"1992","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, Berlin, 1992."},{"key":"20_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"330","DOI":"10.1007\/3-540-48294-6_22","volume-title":"Proceedings of the International Static Analysis Symposium (SAS\u2019 99)","author":"M. M\u00fcller-Olm","year":"1999","unstructured":"M. M\u00fcller-Olm, D. Schmidt, and B. Steffen. Model-checking. A tutorial introduction. In G. Fil\u00e9, editor, Proceedings of the International Static Analysis Symposium (SAS\u2019 99), volume 1694 of Lecture Notes in Computer Science, pages 330\u2013354. Springer-Verlag, Berlin, 1999."},{"key":"20_CR18","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1145\/154630.154648","volume-title":"Proc. of the ACM Symp. on Partial Evaluation and Program Manipulation (PEPM\u2019 93)","author":"A. Mycroft","year":"1993","unstructured":"A. Mycroft. Completeness and predicate-based abstract interpretation. In Proc. of the ACM Symp. on Partial Evaluation and Program Manipulation (PEPM\u2019 93), pages 179\u2013185. ACM Press, New York, 1993."},{"key":"20_CR19","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of European Symposium on Programming (ESOP\u2019 01)","author":"F. Ranzato","year":"2001","unstructured":"F. Ranzato. On the completeness of model checking. In Proc. of European Symposium on Programming (ESOP\u2019 01), Lecture Notes in Computer Science. Springer-Verlag, Berlin, 2001."},{"key":"20_CR20","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1145\/268946.268950","volume-title":"Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL\u2019 98)","author":"D. A. Schmidt","year":"1998","unstructured":"D. A. Schmidt. Data flow analysis is model checking of abstract interpretation. In Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL\u2019 98), pages 38\u201348. ACM Press, New York, 1998."},{"issue":"3","key":"20_CR21","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1023\/A:1007734417713","volume":"10","author":"D. A. Schmidt","year":"1998","unstructured":"D. A. Schmidt. Trace-based abstract interpretation of operational semantics. Lisp and Symbolic Computation, 10(3):237\u2013271, 1998.","journal-title":"Lisp and Symbolic Computation"},{"key":"20_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1007\/3-540-54415-1_54","volume-title":"Proc. of Theoretical aspects of computer software (TACS\u2019 91)","author":"B. Steffen","year":"1991","unstructured":"B. Steffen. Data flow analysis as model checking. In A. Meyer, editor, Proc. of Theoretical aspects of computer software (TACS\u2019 91), volume 526 of Lecture Notes in Computer Science, pages 346\u2013364. Springer-Verlag, Berlin, 1991."}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-47764-0_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T09:32:15Z","timestamp":1558258335000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-47764-0_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540423140","9783540477648"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-47764-0_20","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"4 July 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}