{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,28]],"date-time":"2026-07-28T01:30:39Z","timestamp":1785202239706,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540676287","type":"print"},{"value":"9783540451488","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10720327_5","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T17:52:22Z","timestamp":1167414742000},"page":"62-81","source":"Crossref","is-referenced-by-count":34,"title":["Infinite State Model Checking by Abstract Interpretation and Program Specialisation"],"prefix":"10.1007","author":[{"given":"Michael","family":"Leuschel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thierry","family":"Massart","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-4376-0","volume-title":"Verification of Sequential and Concurrent Programs","author":"K. Apt","year":"1991","unstructured":"Apt, K., Olderog, E.: Verification of Sequential and Concurrent Programs. Springer, Heidelberg (1991)"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BFb0028755","volume-title":"Computer Aided Verification","author":"S. Bensalem","year":"1998","unstructured":"Bensalem, S., Lakhnech, Y., Owre, S.: Computing abstractions of infinite state systems compositionally and automatically. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 319\u2013331. Springer, Heidelberg (1998)"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/3-540-48320-9_14","volume-title":"CONCUR\u201999. Concurrency Theory","author":"B. B\u00e9rard","year":"1999","unstructured":"B\u00e9rard, B., Fribourg, L.: Reachability analysis of (timed) Petri nets using real arithmetic. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, pp. 178\u2013193. Springer, Heidelberg (1999)"},{"key":"5_CR4","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/0743-1066(94)90026-4","volume":"19 & 20","author":"A. Bossi","year":"1994","unstructured":"Bossi, A., Gabrielli, M., Levi, G., Martelli, M.: The s-semantics approach: Theory and applications. The Journal of Logic Programming\u00a019 & 20, 149\u2013198 (1994)","journal-title":"The Journal of Logic Programming"},{"issue":"3","key":"5_CR5","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R. Bryant","year":"1992","unstructured":"Bryant, R.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys\u00a024(3), 293\u2013318 (1992)","journal-title":"ACM Computing Surveys"},{"key":"5_CR6","unstructured":"Burkart, O., Ezparza, J.: More infinite results. In: Proceedings of Infinity 1996, Research Report MIP-9614, University of Passau (1996)"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/BFb0054183","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"W. Charatonik","year":"1998","unstructured":"Charatonik, W., Podelski, A.: Set-based analysis of reactive infinite-state systems. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 358\u2013375. Springer, Heidelberg (1998)"},{"issue":"2","key":"5_CR8","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finitestate concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"4","key":"5_CR9","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"E.M. Clarke","year":"1996","unstructured":"Clarke, E.M., Wing, J.M.: Formal methods: State of the art and future directions. ACM Computing Surveys\u00a028(4), 626\u2013643 (1996)","journal-title":"ACM Computing Surveys"},{"issue":"2 & 3","key":"5_CR10","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/S0743-1066(99)00030-8","volume":"41","author":"D. Schreye De","year":"1999","unstructured":"De Schreye, D., Gl\u00fcck, R., J\u00f8rgensen, J., Leuschel, M., Martens, B., S\u00f8rensen, M.H.: Conjunctive partial deduction: Foundations, control, algorithms and experiments. The Journal of Logic Programming\u00a041(2 & 3), 231\u2013277 (1999)","journal-title":"The Journal of Logic Programming"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"5_CR12","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s002360050074","volume":"34","author":"J. Ezparza","year":"1997","unstructured":"Ezparza, J.: Decidability of model-checking for infinite-state concurrent systems. Acta Informatica\u00a034, 85\u2013107 (1997)","journal-title":"Acta Informatica"},{"issue":"3 & 4","key":"5_CR13","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/BF03037167","volume":"9","author":"J. Gallagher","year":"1991","unstructured":"Gallagher, J., Bruynooghe, M.: The derivation of an algorithm for program specialisation. New Generation Computing\u00a09(3 & 4), 305\u2013333 (1991)","journal-title":"New Generation Computing"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/3-540-46562-6_8","volume-title":"Perspectives of System Informatics","author":"R. Gl\u00fcck","year":"2000","unstructured":"Gl\u00fcck, R., Leuschel, M.: Abstraction-based partial deduction for solving inverse problems - A transformational approach to software verification. In: Bjorner, D., Broy, M., Zamulin, A.V. (eds.) PSI 1999. LNCS, vol.\u00a01755, pp. 93\u2013100. Springer, Heidelberg (2000)"},{"key":"5_CR15","unstructured":"Hartel, P., Butler, M., Currie, A., Henderson, P., Leuschel, M., Martin, A., Smith, A., Ultes-Nitsche, U., Walters, B.: Questions and Answers About Ten Formal Methods. In: Proceedings of FMICS 1999, Trento, Italy (1999)"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/BFb0056612","volume-title":"Principles of Declarative Programming","author":"J. Hatcliff","year":"1998","unstructured":"Hatcliff, J., Dwyer, M.B., Laubach, S.: Staging static analyses using abstraction-based program specialization. In: Palamidessi, C., Meinke, K., Glaser, H. (eds.) ALP 1998 and PLILP 1998. LNCS, vol.\u00a01490, pp. 134\u2013151. Springer, Heidelberg (1998)"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/3-540-60472-3_14","volume-title":"Hybrid Systems II","author":"T.A. Henzinger","year":"1995","unstructured":"Henzinger, T.A., Ho, P.-H.: HYTECH: The Cornell HYbrid TECHnology tool. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S.S. (eds.) HS 1994. LNCS, vol.\u00a0999, pp. 265\u2013293. Springer, Heidelberg (1995)"},{"key":"5_CR18","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1112\/plms\/s3-2.1.326","volume":"2","author":"G. Higman","year":"1952","unstructured":"Higman, G.: Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society\u00a02, 326\u2013336 (1952)","journal-title":"Proceedings of the London Mathematical Society"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/3-540-61580-6_12","volume-title":"Partial Evaluation","author":"J. J\u00f8rgensen","year":"1996","unstructured":"J\u00f8rgensen, J., Leuschel, M.: Efficiently generating efficient generating extensions in Prolog. In: Danvy, O., Thiemann, P., Gl\u00fcck, R. (eds.) Dagstuhl Seminar 1996. LNCS, vol.\u00a01110, pp. 238\u2013262. Springer, Heidelberg (1996)"},{"key":"5_CR20","first-page":"210","volume":"95","author":"J.B. Kruskal","year":"1960","unstructured":"Kruskal, J.B.: Well-quasi ordering, the tree theorem, and Vazsonyi\u2019s conjecture. Transactions of the American Mathematical Society\u00a095, 210\u2013225 (1960)","journal-title":"Transactions of the American Mathematical Society"},{"key":"5_CR21","doi-asserted-by":"crossref","first-page":"587","DOI":"10.1016\/B978-0-934613-40-8.50019-1","volume-title":"Foundations of Deductive Databases and Logic Programming","author":"J.-L. Lassez","year":"1988","unstructured":"Lassez, J.-L., Maher, M., Marriott, K.: Unification revisited. In: Minker, J. (ed.) Foundations of Deductive Databases and Logic Programming, pp. 587\u2013625. Morgan-Kaufmann, San Francisco (1988)"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/3-540-48958-4_11","volume-title":"Logic-Based Program Synthesis and Transformation","author":"M. Leuschel","year":"1999","unstructured":"Leuschel, M.: Improving homeomorphic embedding for online termination. In: Flener, P. (ed.) LOPSTR 1998. LNCS, vol.\u00a01559, pp. 199\u2013218. Springer, Heidelberg (1999)"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/3-540-49727-7_14","volume-title":"Static Analysis","author":"M. Leuschel","year":"1998","unstructured":"Leuschel, M.: On the power of homeomorphic embedding for online termination. In: Levi, G. (ed.) SAS 1998. LNCS, vol.\u00a01503, pp. 230\u2013245. Springer, Heidelberg (1998)"},{"key":"5_CR24","first-page":"220","volume-title":"Proceedings of JICSLP 1998","author":"M. Leuschel","year":"1998","unstructured":"Leuschel, M.: Program specialisation and abstract interpretation reconciled. In: Jaffar, J. (ed.) Proceedings of JICSLP 1998, Manchester, UK, June, pp. 220\u2013234. MIT Press, Cambridge (1998)"},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/3-540-61756-6_82","volume-title":"Programming Languages: Implementations, Logics, and Programs","author":"M. Leuschel","year":"1996","unstructured":"Leuschel, M., De Schreye, D.: Logic program specialisation: How to be more specific. In: Kuchen, H., Swierstra, S.D. (eds.) PLILP 1996. LNCS, vol.\u00a01140, pp. 137\u2013151. Springer, Heidelberg (1996)"},{"key":"5_CR26","unstructured":"Leuschel, M., J\u00f8rgensen, J.: Efficient specialisation in Prolog using a handwritten compiler generator. Technical Report DSSE-TR-99-6, Department of Electronics and Computer Science, University of Southampton (September 1999)"},{"issue":"1","key":"5_CR27","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1145\/271510.271525","volume":"20","author":"M. Leuschel","year":"1998","unstructured":"Leuschel, M., Martens, B., De Schreye, D.: Controlling generalisation and polyvariance in partial deduction of normal logic programs. ACM Transactions on Programming Languages and Systems\u00a020(1), 208\u2013258 (1998)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/BFb0054161","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"X. Liu","year":"1998","unstructured":"Liu, X., Ramakrishnan, C.R., Smolka, S.A.: Fully local and efficient evaluation of alternating fixed points (Extended abstract). In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 5\u201319. Springer, Heidelberg (1998)"},{"issue":"3 & 4","key":"5_CR29","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0743-1066(91)90027-M","volume":"11","author":"J.W. Lloyd","year":"1991","unstructured":"Lloyd, J.W., Shepherdson, J.C.: Partial evaluation in logic programming. The Journal of Logic Programming\u00a011(3 & 4), 217\u2013242 (1991)","journal-title":"The Journal of Logic Programming"},{"key":"5_CR30","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/BF01531082","volume":"1","author":"K. Marriott","year":"1990","unstructured":"Marriott, K., Naish, L., Lassez, J.-L.: Most specific logic programs. Annals of Mathematics and Artificial Intelligence\u00a01, 303\u2013338 (1990)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"5_CR31","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking. PhD thesis, Boston (1993)","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"5_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/3-540-61604-7_56","volume-title":"CONCUR 1996: Concurrency Theory","author":"F. Moller","year":"1996","unstructured":"Moller, F.: Infinite results. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol.\u00a01119, pp. 195\u2013216. Springer, Heidelberg (1996)"},{"key":"5_CR33","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1145\/259380.259419","volume-title":"Proceedings of PODC 1997","author":"U. Nitsche","year":"1997","unstructured":"Nitsche, U., Wolper, P.: Relative liveness and behavior abstraction. In: Proceedings of PODC 1997, Santa Barbara, California, pp. 45\u201352. ACM, New York (1997)"},{"issue":"2","key":"5_CR34","first-page":"167","volume":"5","author":"T.C. Przymusinksi","year":"1989","unstructured":"Przymusinksi, T.C.: On the declarative and procedural semantics of logic programs. Journal of Automated Reasoning\u00a05(2), 167\u2013205 (1989)","journal-title":"Journal of Automated Reasoning"},{"key":"5_CR35","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"Y.S. Ramakrishna","year":"1997","unstructured":"Ramakrishna, Y.S., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., Swift, T., Warrend, D.S.: Efficient model checking using tabled resolution. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254. Springer, Heidelberg (1997)"},{"key":"5_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/3-540-48119-2_3","volume-title":"FM\u201999 - Formal Methods","author":"J. Rushby","year":"1999","unstructured":"Rushby, J.: Mechanized formal methods: Where next? In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01708, pp. 48\u201351. Springer, Heidelberg (1999)"},{"key":"5_CR37","first-page":"442","volume-title":"Proceedings of the ACM SIGMOD International Conference on the Management of Data","author":"K. Sagonas","year":"1994","unstructured":"Sagonas, K., Swift, T., Warren, D.S.: XSB as an efficient deductive database engine. In: Proceedings of the ACM SIGMOD International Conference on the Management of Data, Minneapolis, Minnesota, pp. 442\u2013453. ACM, New York (1994)"},{"key":"5_CR38","first-page":"465","volume-title":"Proceedings of ILPS 1995","author":"M.H. S\u00f8rensen","year":"1995","unstructured":"S\u00f8rensen, M.H., Gl\u00fcck, R.: An algorithm of generalization in positive supercompilation. In: Lloyd, J.W. (ed.) Proceedings of ILPS 1995, Portland, USA, December 1995, pp. 465\u2013479. MIT Press, Cambridge (1995)"},{"key":"5_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/BFb0028736","volume-title":"Computer Aided Verification","author":"P. Wolper","year":"1998","unstructured":"Wolper, P., Boigelot, B.: Verifying systems with infinite but regular state spaces. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 88\u201397. Springer, Heidelberg (1998)"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10720327_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T11:39:38Z","timestamp":1556019578000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10720327_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676287","9783540451488"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/10720327_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000]]}}}