{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,7]],"date-time":"2026-07-07T22:20:48Z","timestamp":1783462848704,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540678397","type":"print"},{"value":"9783540449140","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44914-0_1","type":"book-chapter","created":{"date-parts":[[2007,5,22]],"date-time":"2007-05-22T17:26:14Z","timestamp":1179854774000},"page":"1-25","source":"Crossref","is-referenced-by-count":27,"title":["Partial Completeness of Abstract Fixpoint Checking"],"prefix":"10.1007","author":[{"given":"Patrick","family":"Cousot","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2000,8,11]]},"reference":[{"key":"1_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1007\/3-540-48683-6_15","volume-title":"Proceedings of the Eleventh International Conference on Computer Aided Verification, CAV\u2019 99","author":"P.A. Abdulla","year":"1999","unstructured":"P.A. Abdulla, A. Annichini, S. Bensalem, A. Bouajjani, P. Habermehl, and L. Lakhnech. Verification of infinite-state systems by combining abstraction and reachability analysis. In N. Halbwachs and D. Peled, editors, Proceedings of the Eleventh International Conference on Computer Aided Verification, CAV\u2019 99, Trento, Italy, Lecture Notes in Computer Science 1633, pages 146\u2013159. Springer-Verlag, Berlin, Germany, 6\u201310 July 1999."},{"key":"1_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BFb0028755","volume-title":"Proceedings of the Tenth International Conference on Computer Aided Verification, CAV\u2019 98","author":"S. Bensalem","year":"1998","unstructured":"S. Bensalem, Y. Lakhnech, and S. Owre. Computing abstractions of infinite state systems compositionally and automatically. In A.J. Hu and M.Y. Vardi, editors, Proceedings of the Tenth International Conference on Computer Aided Verification, CAV\u2019 98, Vancouver, British Columbia, Canada, Lecture Notes in Computer Science 1427, pages 319\u2013331. Springer-Verlag, Berlin, Germany, 28 June\u20132 July 1998."},{"key":"1_CR3","series-title":"Lect Notes Comput Sci","volume-title":"IBM Workshop on Logics of Programs","author":"E.M. Clarke","year":"1981","unstructured":"E.M. Clarke and E. A. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. In IBM Workshop on Logics of Programs, Lecture Notes in Computer Science 131. Springer-Verlag, Berlin, Germany, May 1981."},{"issue":"5","key":"1_CR4","doi-asserted-by":"crossref","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 Transactions on Programming Languages and Systems, 16(5):1512\u20131542, september 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"1_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/BFb0028753","volume-title":"Proceedings of the Tenth International Conference on Computer Aided Verification, CAV\u2019 98","author":"M. Col\u00f3n","year":"1998","unstructured":"M. Col\u00f3n and T.E. Uribe. Generating finite-state abstractions of reactive systems using decision procedures. In A.J. Hu and M.Y. Vardi, editors, Proceedings of the Tenth International Conference on Computer Aided Verification, CAV\u2019 98, Vancouver, British Columbia, Canada, Lecture Notes in Computer Science 1427, pages 293\u2013304. Springer-Verlag, Berlin, Germany, 28 June\u20132 July 1998."},{"key":"1_CR6","unstructured":"P. Cousot. M\u00e9thodes it\u00e9ratives de construction et d\u2019approximation de points fixes d\u2019op\u00e9rateurs monotones sur un treillis, analyse s\u00e9mantique de programmes. Th\u00e9se d\u2019\u00c9tat es sciences math\u00e9matiques, Universit\u00e9 scientifique et m\u00e9dicale de Grenoble, Grenoble, 21 mars 1978."},{"key":"1_CR7","first-page":"303","volume-title":"Program Flow Analysis: Theory and Applications","author":"P. Cousot","year":"1981","unstructured":"P. Cousot. Semantic foundations of program analysis. In S.S. Muchnick and N.D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 10, pages 303\u2013342. Prentice-Hall, Inc., Englewood Cliffs, New Jersey, United States, 1981."},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"P. Cousot. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Electronic Notes in Theoretical Computer Science, 6, 1997. URL: http:\/\/www.elsevier.nl\/locate\/entcs\/volume6.html , 25 pages.","DOI":"10.1016\/S1571-0661(05)80168-9"},{"key":"1_CR9","unstructured":"P. Cousot. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theoretical Computer Science, To appear (Preliminary version in [8])."},{"key":"1_CR10","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1145\/512950.512973","volume-title":"Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","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 Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 238\u2013252, Los Angeles, California, 1977. ACM Press, New York, New York, United States."},{"issue":"1","key":"1_CR11","doi-asserted-by":"crossref","first-page":"43","DOI":"10.2140\/pjm.1979.82.43","volume":"82","author":"P. Cousot","year":"1979","unstructured":"P. Cousot and R. Cousot. Constructive versions of Tarski\u2019s fixed point theorems. Pacific Journal of Mathematics, 82(1):43\u201357, 1979.","journal-title":"Pacific Journal of Mathematics"},{"key":"1_CR12","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1145\/567752.567778","volume-title":"Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"P. Cousot","year":"1979","unstructured":"P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 269\u2013282, San Antonio, Texas, 1979. ACM Press, New York, New York, United States."},{"key":"1_CR13","first-page":"43","volume-title":"Tools & Notions for Program Construction","author":"P. Cousot","year":"1982","unstructured":"P. Cousot and R. Cousot. Induction principles for proving invariance properties of programs. In D. N\u00e9el, editor, Tools & Notions for Program Construction, pages 43\u2013119. Cambridge University Press, Cambridge, United Kindom, 1982."},{"issue":"2\u20133","key":"1_CR14","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0743-1066(92)90030-7","volume":"13","author":"P. Cousot","year":"1992","unstructured":"P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. Journal of Logic Programming, 13(2\u20133):103\u2013179, 1992. (The editor of Journal of Logic Programming has mistakenly published the unreadable galley proof. For a correct version of this paper, see http:\/\/www.di.ens.fr\/~cousot ).","journal-title":"Journal of Logic Programming"},{"key":"1_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/3-540-55844-6_142","volume-title":"Proceedings of the International Workshop Programming Language Implementation and Logic Programming, PLILP\u2019 92","author":"P. Cousot","year":"1992","unstructured":"P. Cousot and R. Cousot. Comparing the Galois connection and widening\/ narrowing approaches to abstract interpretation, invited paper. In M. Bruynooghe and M. Wirsing, editors, Proceedings of the International Workshop Programming Language Implementation and Logic Programming, PLILP\u2019 92, Leuven, Belgium, 13\u201317 August 1992, Lecture Notes in Computer Science 631, pages 269\u2013295. Springer-Verlag, Berlin, Germany, 1992."},{"key":"1_CR16","first-page":"91","volume-title":"Proceedings of the First ACM SIGPLAN Workshop on Automatic Analysis of Software, AAS\u2019 97","author":"P. Cousot","year":"1997","unstructured":"P. Cousot and R. Cousot. Parallel combination of abstract interpretation and model-based automatic analysis of software. In R. Cleaveland and D. Jackson, editors, Proceedings of the First ACM SIGPLAN Workshop on Automatic Analysis of Software, AAS\u2019 97, pages 91\u201398, Paris, France, January 1997. ACM Press, New York, New York, United States."},{"key":"1_CR17","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:69\u201395, 1999.","journal-title":"Automated Software Engineering"},{"key":"1_CR18","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, Massachusetts, January 2000. ACM Press, New York, New York, United States."},{"issue":"2","key":"1_CR19","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"D. Dams","year":"1997","unstructured":"D. Dams, O. Grumberg, and R. Gerth. Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems, 19(2):253\u2013291, 1997.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"1_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1007\/3-540-48683-6_16","volume-title":"Proceedings of the Eleventh International Conference on Computer Aided Verification, CAV\u2019 99","author":"S. Das","year":"1999","unstructured":"S. Das, D.L. Dill, and S. Park. Experience with predicate abstraction. In N. Halbwachs and D. Peled, editors, Proceedings of the Eleventh International Conference on Computer Aided Verification, CAV\u2019 99, Trento, Italy, Lecture Notes in Computer Science 1633, pages 160\u2013171. Springer-Verlag, Berlin, Germany, 6\u201310 July 1999."},{"key":"1_CR21","first-page":"19","volume-title":"Proceedings of the Symposium in Applied Mathematics","author":"R.W. Floyd","year":"1967","unstructured":"R.W. Floyd. Assigning meaning to programs. In J.T. Schwartz, editor, Proceedings of the Symposium in Applied Mathematics, volume 19, pages 19\u201332. American Mathematical Society, Providence, Rhode Island, United States, 1967."},{"key":"1_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/BFb0055786","volume-title":"Proceedings of the Twentythird International Symposium on Mathematical Foundations of Computer Science, MFCS\u201998","author":"R. Giacobazzi","year":"1998","unstructured":"R. Giacobazzi, F. Ranzato, and F. Scozzari. Complete abstract interpretations made constructive. In L. Brim, J. Gruska, and J. Zlatuska, editors, Proceedings of the Twentythird International Symposium on Mathematical Foundations of Computer Science, MFCS\u201998, volume 1450 of Lecture Notes in Computer Science, pages 366\u2013377. Springer-Verlag, Berlin, Germany, 1998."},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract intrepretations complete. Journal of the Association for Computing Machinary, 2000. To appear.","DOI":"10.1145\/333979.333989"},{"key":"1_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1007\/3-540-56922-7_7","volume-title":"Proceedings of the Fifth International Conference on Computer Aided Verification, CAV\u2019 93","author":"S. Graf","year":"1993","unstructured":"S. Graf and C. Loiseaux. A tool for symbolic program verification and abstraction. In C. Courcoubetis, editor, Proceedings of the Fifth International Conference on Computer Aided Verification, CAV\u2019 93, Elounda, Greece, Lecture Notes in Computer Science 697, pages 71\u201384. Springer-Verlag, Berlin, Germany, 28 June\u20131 July 1993."},{"key":"1_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Proceedings of the Ninth International Conference on Computer Aided Verification, CAV\u201997","author":"S. Graf","year":"1997","unstructured":"S. Graf and H. Sa\u00efdi. Construction of abstract state graphs with PVS. In O. Grumberg, editor, Proceedings of the Ninth International Conference on Computer Aided Verification, CAV\u201997, Haifa, Israel, Lecture Notes in Computer Science 1254, pages 72\u201383. Springer-Verlag, Berlin, Germany, 22\u201325 July 1997."},{"key":"1_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/BFb0028745","volume-title":"Proceedings of the Tenth International Conference on Computer Aided Verification, CAV\u2019 98","author":"T.A. Henzinger","year":"1998","unstructured":"T.A. Henzinger, O. Kupferman, and S. Qadeer. From Pre-historic to Post-modern symbolic model checking. In A.J. Hu and M.Y. Vardi, editors, Proceedings of the Tenth International Conference on Computer Aided Verification, CAV\u2019 98, Vancouver, British Columbia, Canada, Lecture Notes in Computer Science 1427, pages 195\u2013206. Springer-Verlag, Berlin, Germany, June \/July 1998."},{"key":"1_CR27","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/BFb0055757","volume-title":"Twentythird International Symposium on Mathematical Foundations of Computer Science 1998","author":"Y. Kesten","year":"1998","unstructured":"Y. Kesten and A. Pnueli. Modularization and abstraction: The keys to formal verification. In L. Brim, J. Gruska, and J. Zlatuska, editors, Twentythird International Symposium on Mathematical Foundations of Computer Science 1998, Lecture Notes in Computer Science 1450, pages 54\u201371. Springer-Verlag, Berlin, Germany, 1998."},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6(1), 1995.","DOI":"10.1007\/BF01384313"},{"key":"1_CR29","unstructured":"D. Monniaux. R\u00e9alisation m\u00e9canis\u00e9e d\u2019interpr\u00e9teurs abstraits. Rapport de stage, DEA \u201cS\u00e9mantique, Preuve et Programmation\u201d, July 1998."},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"J.H. Morris and B. Wegbreit. Sungoal induction. Communications of the Association for Computing Machinary, 20(4):209\u2013222, April 1977.","DOI":"10.1145\/359461.359466"},{"key":"1_CR31","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/BF01966091","volume":"6","author":"P. Naur","year":"1966","unstructured":"P. Naur. Proofs of algorithms by general snapshots. BIT, 6:310\u2013316, 1966.","journal-title":"BIT"},{"key":"1_CR32","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"Proceedings of the International Symposium on Programming","author":"J.-P. Queille","year":"1982","unstructured":"J.-P. Queille and J. Sifakis. Verification of concurrent systems in Cesar. In Proceedings of the International Symposium on Programming, Lecture Notes in Computer Science 137, pages 337\u2013351. Springer-Verlag, Berlin, Germany, 1982."},{"key":"1_CR33","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1007\/3-540-48683-6_38","volume-title":"Proceedings of the Eleventh International Conference on Computer Aided Verification, CAV\u201999","author":"H. Sa\u00efdi","year":"1999","unstructured":"H. Sa\u00efdi and N. Shankar. Abstract and model check while you prove. In N. Halbwachs and D. Peled, editors, Proceedings of the Eleventh International Conference on Computer Aided Verification, CAV\u201999, Trento, Italy, Lecture Notes in Computer Science 1633, pages 443\u2013454. Springer-Verlag, Berlin, Germany, 6\u201310 July 1999."},{"key":"1_CR34","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","unstructured":"A. Tarski. A lattice theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285\u2013310, 1955.","journal-title":"Pacific Journal of Mathematics"}],"container-title":["Lecture Notes in Computer Science","Abstraction, Reformulation, and Approximation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44914-0_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T03:01:26Z","timestamp":1556420486000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44914-0_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678397","9783540449140"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/3-540-44914-0_1","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2000]]}}}