{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,23]],"date-time":"2025-02-23T05:04:52Z","timestamp":1740287092965,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":77,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642143083"},{"type":"electronic","value":"9783642143090"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14309-0_7","type":"book-chapter","created":{"date-parts":[[2010,6,23]],"date-time":"2010-06-23T13:09:58Z","timestamp":1277298598000},"page":"136-158","source":"Crossref","is-referenced-by-count":3,"title":["Static Analysis, Abstract Interpretation and Verification in (Constraint Logic) Programming"],"prefix":"10.1007","author":[{"given":"Giorgio","family":"Delzanno","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Giacobazzi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francesco","family":"Ranzato","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3\/4","key":"7_CR1","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1007\/BF03037173","volume":"9","author":"J.-M. Andreoli","year":"1991","unstructured":"Andreoli, J.-M., Pareschi, R.: Linear Ojects. Logical Processes with Built-in Inheritance. New Generation Comput.\u00a09(3\/4), 445\u2013474 (1991)","journal-title":"New Generation Comput."},{"key":"7_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-540-73595-3_28","volume-title":"Automated Deduction \u2013 CADE-21","author":"D. Baelde","year":"2007","unstructured":"Baelde, D., Gacek, A., Miller, D., Nadathur, G., Tiu, A.: The Bedwyr system for model checking over syntactic expressions. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 391\u2013397. Springer, Heidelberg (2007)"},{"issue":"1-2","key":"7_CR3","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(00)00312-1","volume":"277","author":"R. Bagnara","year":"2002","unstructured":"Bagnara, R., Hill, P., Zaffanella, E.: Set-sharing is redundant for pair-sharing. Theor. Comput. Sci.\u00a0277(1-2), 3\u201346 (2002)","journal-title":"Theor. Comput. Sci."},{"issue":"5-6","key":"7_CR4","first-page":"573","volume":"4","author":"M. Bozzano","year":"2004","unstructured":"Bozzano, M., Delzanno, G., Martelli, M.: Model Checking Linear Logic Specifications. TPLP\u00a04(5-6), 573\u2013619 (2004)","journal-title":"TPLP"},{"key":"7_CR5","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M.C. Browne","year":"1988","unstructured":"Browne, M.C., Clarke, E.M., Grumberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theoret. Comp. Sci.\u00a059, 115\u2013131 (1988)","journal-title":"Theoret. Comp. Sci."},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic Model Checking: 1020 States and Beyond. In: Proc. IEEE LICS 1990, pp. 428\u2013439 (1990)","DOI":"10.1109\/LICS.1990.113767"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Cervesato, I.: Typed Multiset Rewriting Specifications of Security Protocols. ENTCS\u00a040 (2000)","DOI":"10.1016\/S1571-0661(05)80035-0"},{"key":"7_CR8","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":"7_CR9","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":"7_CR10","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)"},{"issue":"1","key":"7_CR11","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/239912.239914","volume":"19","author":"A. Cortesi","year":"1997","unstructured":"Cortesi, A., Fil\u00e9, G., Giacobazzi, R., Palamidessi, C., Ranzato, F.: Complementation in abstract interpretation. ACM Trans. Program. Lang. Syst.\u00a019(1), 7\u201347 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1-3","key":"7_CR12","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/S0167-6423(99)00045-3","volume":"38","author":"A. Cortesi","year":"2000","unstructured":"Cortesi, A., Le Charlier, B., Van Hentenryck, P.: Combinations of abstract domains for logic programming: open product and generic pattern construction. Sci. Comput. Program.\u00a038(1-3), 27\u201371 (2000)","journal-title":"Sci. Comput. Program."},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Cousot, P.: Types as abstract interpretations (invited paper). In: Proc. ACM POPL 1997, pp. 316\u2013331 (1997)","DOI":"10.1145\/263699.263744"},{"issue":"1-2","key":"7_CR14","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/S0304-3975(00)00313-3","volume":"277","author":"P. Cousot","year":"2002","unstructured":"Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theor. Comput. Sci.\u00a0277(1-2), 47\u2013103 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR15","first-page":"238","volume-title":"Proc. of Conf. Record of the 4th ACM Symp. on Principles of Programming Languages (POPL\u00a0 1977)","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. of Conf. Record of the 4th ACM Symp. on Principles of Programming Languages (POPL\u00a0 1977), pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"7_CR16","first-page":"269","volume-title":"Proc. of Conf. Record of the 6th ACM Symp. on Principles of Programming Languages (POPL 1979)","author":"P. Cousot","year":"1979","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. of Conf. Record of the 6th ACM Symp. on Principles of Programming Languages (POPL 1979), pp. 269\u2013282. ACM Press, New York (1979)"},{"issue":"2-3","key":"7_CR17","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0743-1066(92)90030-7","volume":"13","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. J. Logic Program.\u00a013(2-3), 103\u2013179 (1992)","journal-title":"J. Logic Program."},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages) (invited paper). In: Proc. of the 1994 IEEE Internat. Conf. on Computer Languages (ICCL 1994), pp. 95\u2013112 (1994)","DOI":"10.1109\/ICCL.1994.288389"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Temporal abstract interpretation. In: Proc. 27th ACM POPL, pp. 12\u201325 (2000)","DOI":"10.1145\/325694.325699"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"P. Cousot","year":"2005","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The ASTRE\u00c9 analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 21\u201330. Springer, Heidelberg (2005)"},{"issue":"46","key":"7_CR21","doi-asserted-by":"publisher","first-page":"4724","DOI":"10.1016\/j.tcs.2009.07.040","volume":"410","author":"P. Cousot","year":"2009","unstructured":"Cousot, P., Cousot, R., Giacobazzi, R.: Abstract interpretation of resolution-based semantics. Theor. Comput. Sci.\u00a0410(46), 4724\u20134746 (2009)","journal-title":"Theor. Comput. Sci."},{"issue":"5","key":"7_CR22","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":"7_CR23","doi-asserted-by":"crossref","unstructured":"Delzanno, G.: An Overview of MSR(C): A CLP-based Framework for the Symbolic Verification of Parameterized Concurrent Systems. ENTCS\u00a076 (2002)","DOI":"10.1016\/S1571-0661(04)80786-2"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-49059-0_16","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"G. Delzanno","year":"1999","unstructured":"Delzanno, G., Podelski, A.: Model Checking in CLP. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 223\u2013239. Springer, Heidelberg (1999)"},{"key":"7_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/3-540-49059-0_6","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"Y. Dong","year":"1999","unstructured":"Dong, Y., Du, X., Ramakrishna, Y.S., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., Sokolsky, O., Stark, E.W., Scott Warren, D.: Fighting Livelock in the i-Protocol: A Comparative Study of Verification Tools. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 74\u201388. Springer, Heidelberg (1999)"},{"issue":"3","key":"7_CR26","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1016\/0304-3975(89)90070-4","volume":"69","author":"M. Falaschi","year":"1989","unstructured":"Falaschi, M., Levi, G., Palamidessi, C., Martelli, M.: Declarative modeling of the operational behavior of logic languages. Theor. Comput. Sci.\u00a069(3), 289\u2013318 (1989)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"7_CR27","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1145\/234528.234742","volume":"28","author":"G. Fil\u00e9","year":"1996","unstructured":"Fil\u00e9, G., Giacobazzi, R., Ranzato, F.: A unifying view of abstract domain design. ACM Comput. Surv.\u00a028(2), 333\u2013336 (1996)","journal-title":"ACM Comput. Surv."},{"key":"7_CR28","unstructured":"Fil\u00e9, G., Ranzato, F.: Complementation of abstract domains made easy. In: Proc. of the 1996 Joint Internat. Conf. and Symp. on Logic Programming (JICSLP\u00a01996), pp. 348\u2013362 (1996)"},{"key":"7_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/3-540-45607-4_7","volume-title":"Logic Based Program Synthesis and Transformation","author":"F. Fioravanti","year":"2002","unstructured":"Fioravanti, F., Pettorossi, A., Proietti, M.: Verification of Sets of Infinite State Processes Using Program Transformation. In: Pettorossi, A. (ed.) LOPSTR 2001. LNCS, vol.\u00a02372, pp. 111\u2013128. Springer, Heidelberg (2002)"},{"key":"7_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1007\/3-540-62718-9_2","volume-title":"Logic Program Synthesis and Transformation","author":"L. Fribourg","year":"1997","unstructured":"Fribourg, L., Richardson, J.: Symbolic Verification with Gap-Order Constraints. In: Gallagher, J.P. (ed.) LOPSTR 1996. LNCS, vol.\u00a01207, pp. 20\u201337. Springer, Heidelberg (1997)"},{"issue":"3\/4","key":"7_CR31","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1023\/A:1009747629591","volume":"2","author":"L. Fribourg","year":"1997","unstructured":"Fribourg, L., Ols\u00e9n, H.: A Decompositional Approach for Computing Least Fixed-Points of Datalog Programs with Z-Counters. Constraints\u00a02(3\/4), 305\u2013335 (1997)","journal-title":"Constraints"},{"issue":"1","key":"7_CR32","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1023\/A:1027328830731","volume":"31","author":"R. Gentilini","year":"2003","unstructured":"Gentilini, R., Piazza, C., Policriti, A.: From bisimulation to simulation: coarsest partition problems. J. Automated Reasoning\u00a031(1), 73\u2013103 (2003)","journal-title":"J. Automated Reasoning"},{"key":"7_CR33","doi-asserted-by":"crossref","unstructured":"Giacobazzi, R., Mastroeni, I.: Compositionality in the puzzle of semantics. In: Proc. of the ACM Symp. on Partial Evaluation and Semantics-Based Program Manipulation (PEPM 2002), pp. 87\u201397 (2002)","DOI":"10.1145\/503032.503040"},{"issue":"1-3","key":"7_CR34","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2004.12.021","volume":"337","author":"R. Giacobazzi","year":"2005","unstructured":"Giacobazzi, R., Mastroeni, I.: Transforming semantics by abstract interpretation. Theor. Comput. Sci.\u00a0337(1-3), 1\u201350 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-69166-2_1","volume-title":"Static Analysis","author":"R. Giacobazzi","year":"2008","unstructured":"Giacobazzi, R., Mastroeni, I.: Transforming abstract interpretations by abstract interpretation. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol.\u00a05079, pp. 1\u201317. Springer, Heidelberg (2008)"},{"issue":"3","key":"7_CR36","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/BF01236765","volume":"36","author":"R. Giacobazzi","year":"1996","unstructured":"Giacobazzi, R., Palamidessi, C., Ranzato, F.: Weak relative pseudo-complements of closure operators. Algebra Universalis\u00a036(3), 405\u2013412 (1996)","journal-title":"Algebra Universalis"},{"key":"7_CR37","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)"},{"key":"7_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/3-540-61735-3_16","volume-title":"Algebraic and Logic Programming","author":"R. Giacobazzi","year":"1996","unstructured":"Giacobazzi, R., Ranzato, F.: Complementing logic program semantics. In: Hanus, M., Rodr\u00edguez-Artalejo, M. (eds.) ALP 1996. LNCS, vol.\u00a01139, pp. 238\u2013253. Springer, Heidelberg (1996)"},{"key":"7_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"771","DOI":"10.1007\/3-540-63165-8_230","volume-title":"Automata, Languages and Programming","author":"R. Giacobazzi","year":"1997","unstructured":"Giacobazzi, R., Ranzato, F.: Refining and compressing abstract domains. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol.\u00a01256, pp. 771\u2013781. Springer, Heidelberg (1997)"},{"issue":"1-3","key":"7_CR40","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/S0167-6423(97)00034-8","volume":"32","author":"R. Giacobazzi","year":"1998","unstructured":"Giacobazzi, R., Ranzato, F.: Optimal domains for disjunctive abstract interpretation. Sci. Comput. Program\u00a032(1-3), 177\u2013210 (1998)","journal-title":"Sci. Comput. Program"},{"issue":"2","key":"7_CR41","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1006\/inco.1998.2724","volume":"145","author":"R. Giacobazzi","year":"1998","unstructured":"Giacobazzi, R., Ranzato, F.: Uniform closures: order-theoretically reconstructing logic program semantics and abstract domain refinements. Information and Computation\u00a0145(2), 153\u2013190 (1998)","journal-title":"Information and Computation"},{"key":"7_CR42","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/S0304-3975(98)00194-7","volume":"216","author":"R. Giacobazzi","year":"1999","unstructured":"Giacobazzi, R., Ranzato, F.: The reduced relative power operation on abstract domains. Theor. Comput. Sci\u00a0216, 159\u2013211 (1999)","journal-title":"Theor. Comput. Sci"},{"issue":"3","key":"7_CR43","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1016\/j.ic.2006.01.001","volume":"204","author":"R. Giacobazzi","year":"2006","unstructured":"Giacobazzi, R., Ranzato, F.: Incompleteness of states w.r.t. traces in model checking. Information and Computation\u00a0204(3), 376\u2013407 (2006)","journal-title":"Information and Computation"},{"issue":"2","key":"7_CR44","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1145\/333979.333989","volume":"47","author":"R. Giacobazzi","year":"2000","unstructured":"Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM\u00a047(2), 361\u2013416 (2000)","journal-title":"J. ACM"},{"issue":"1","key":"7_CR45","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1145\/1042038.1042040","volume":"6","author":"R. Giacobazzi","year":"2005","unstructured":"Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract domains condensing. ACM Transactions on Computational Logic\u00a06(1), 33\u201360 (2005)","journal-title":"ACM Transactions on Computational Logic"},{"issue":"5","key":"7_CR46","doi-asserted-by":"publisher","first-page":"1067","DOI":"10.1145\/293677.293680","volume":"20","author":"R. Giacobazzi","year":"1998","unstructured":"Giacobazzi, R., Scozzari, F.: A logical model for relational abstract domains. ACM Trans. Program. Lang. Syst.\u00a020(5), 1067\u20131109 (1998)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/978-3-540-70545-1_49","volume-title":"Computer Aided Verification","author":"R.J. Glabbeek van","year":"2008","unstructured":"van Glabbeek, R.J., Ploeger, B.: Correcting a space-efficient simulation algorithm. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 517\u2013529. Springer, Heidelberg (2008)"},{"key":"7_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1007\/BFb0032063","volume-title":"Automata, Languages and Programming","author":"J.F. Groote","year":"1990","unstructured":"Groote, J.F., Vaandrager, F.: An efficient algorithm for branching bisimulation and stuttering equivalence. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol.\u00a0443, pp. 626\u2013638. Springer, Heidelberg (1990)"},{"key":"7_CR49","doi-asserted-by":"crossref","unstructured":"Gupta, G., Pontelli, E.: A constraint-based approach for specification and verification of real-time systems. In: Proc. IEEE Real-Time Systems Symposium 1997, pp. 230\u2013239 (1997)","DOI":"10.1109\/REAL.1997.641285"},{"key":"7_CR50","doi-asserted-by":"crossref","unstructured":"Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: Proc. 36th FOCS, pp. 453\u2013462 (1995)","DOI":"10.1109\/SFCS.1995.492576"},{"issue":"1","key":"7_CR51","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1042038.1042039","volume":"6","author":"T.A. Henzinger","year":"2005","unstructured":"Henzinger, T.A., Maujumdar, R., Raskin, J.-F.: A classification of symbolic transition systems. ACM Trans. Comput. Log.\u00a06(1), 1\u201331 (2005)","journal-title":"ACM Trans. Comput. Log."},{"issue":"5","key":"7_CR52","doi-asserted-by":"publisher","first-page":"751","DOI":"10.1145\/265943.265966","volume":"19","author":"T.P. Jensen","year":"1997","unstructured":"Jensen, T.P.: Disjunctive program analysis for algebraic data types. ACM Trans. Program. Lang. Syst.\u00a019(5), 751\u2013803 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7_CR53","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/3-540-44957-4_7","volume-title":"Computational Logic - CL 2000","author":"M. Leuschel","year":"2000","unstructured":"Leuschel, M., Lehmann, H.: Coverability of reset petri nets and other well-structured transition systems by partial deduction. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol.\u00a01861, pp. 101\u2013115. Springer, Heidelberg (2000)"},{"key":"7_CR54","doi-asserted-by":"crossref","unstructured":"Leuschel, M., Lehmann, H.: Solving coverability problems of petri nets by partial deduction. In: Proc. PPDP 2000, pp. 268\u2013279 (2000)","DOI":"10.1145\/351268.351298"},{"key":"7_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/10720327_5","volume-title":"Logic-Based Program Synthesis and Transformation","author":"M. Leuschel","year":"2000","unstructured":"Leuschel, M., Massart, T.: Infinite State Model Checking by Abstract Interpretation and Program Specialisation. In: Bossi, A. (ed.) LOPSTR 1999. LNCS, vol.\u00a01817, pp. 62\u201381. Springer, Heidelberg (2000)"},{"key":"7_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/BFb0056613","volume-title":"Principles of Declarative Programming","author":"G. Levi","year":"1998","unstructured":"Levi, G., Spoto, F.: An experiment in domain refinement: Type domains and type representations for logic programs. In: Palamidessi, C., Meinke, K., Glaser, H. (eds.) ALP 1998 and PLILP 1998. LNCS, vol.\u00a01490, pp. 152\u2013169. Springer, Heidelberg (1998)"},{"key":"7_CR57","doi-asserted-by":"crossref","unstructured":"Levi, G., Spoto, F.: Non pair-sharing and freeness analysis through linear refinement. In: Proc. ACM PEPM, pp. 52\u201361 (2000)","DOI":"10.1145\/328691.328699"},{"issue":"1","key":"7_CR58","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1016\/S0890-5401(02)00048-2","volume":"182","author":"G. Levi","year":"2003","unstructured":"Levi, G., Spoto, F.: Pair-independence and freeness analysis through linear refinement. Information and Computation\u00a0182(1), 14\u201352 (2003)","journal-title":"Information and Computation"},{"key":"7_CR59","doi-asserted-by":"crossref","unstructured":"L\u00f3pez, P., Pfenning, F., Polakow, J., Watkins, K.: Monadic concurrent linear logic programming. In: Proc. PPDP 2005, pp. 35\u201346 (2005)","DOI":"10.1145\/1069774.1069778"},{"key":"7_CR60","doi-asserted-by":"crossref","unstructured":"Mycroft, A.: Completeness and predicate-based abstract interpretation. In: Proc. of the ACM Symp. on Partial Evaluation and Program Manipulation (PEPM 1993), pp. 179\u2013185 (1993)","DOI":"10.1145\/154630.154648"},{"key":"7_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/3-540-16446-4_10","volume-title":"Programs as Data Objects","author":"F. Nielson","year":"1986","unstructured":"Nielson, F.: Expected forms of data flow analyses. In: Ganzinger, H., Jones, N.D. (eds.) Programs as Data Objects. LNCS, vol.\u00a0217, pp. 172\u2013191. Springer, Heidelberg (1986)"},{"issue":"6","key":"7_CR62","doi-asserted-by":"publisher","first-page":"977","DOI":"10.1137\/0216062","volume":"16","author":"R. Paige","year":"1987","unstructured":"Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM Journal on Computing\u00a016(6), 977\u2013982 (1987)","journal-title":"SIAM Journal on Computing"},{"key":"7_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/11680093_3","volume-title":"Logic Based Program Synthesis and Transformation","author":"A. Pettorossi","year":"2006","unstructured":"Pettorossi, A., Proietti, M., Senni, V.: Transformational Verification of Parameterized Protocols Using Array Formulas. In: Hill, P.M. (ed.) LOPSTR 2005. LNCS, vol.\u00a03901, pp. 23\u201343. Springer, Heidelberg (2006)"},{"key":"7_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45241-9_1","volume-title":"Practical Aspects of Declarative Languages","author":"C.R. Ramakrishnan","year":"2001","unstructured":"Ramakrishnan, C.R.: A Model Checker for Value-Passing Mu-Calculus Using Logic Programming. In: Ramakrishnan, I.V. (ed.) PADL 2001. LNCS, vol.\u00a01990, pp. 1\u201313. Springer, Heidelberg (2001)"},{"key":"7_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/3-540-63166-6_16","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., Warren, D.S.: Efficient Model Checking Using Tabled Resolution. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 143\u2013154. Springer, Heidelberg (1997)"},{"key":"7_CR66","doi-asserted-by":"crossref","unstructured":"Ranzato, F., Tapparo, F.: A new efficient simulation equivalence algorithm. In: Proc. 22nd IEEE Symp. on Logic in Computer Science (LICS 2007), pp. 171\u2013180 (2007)","DOI":"10.1109\/LICS.2007.8"},{"issue":"5","key":"7_CR67","doi-asserted-by":"publisher","first-page":"620","DOI":"10.1016\/j.ic.2008.01.001","volume":"206","author":"F. Ranzato","year":"2008","unstructured":"Ranzato, F., Tapparo, F.: Generalizing the Paige-Tarjan algorithm by abstract interpretation. Information and Computation\u00a0206(5), 620\u2013651 (2008)","journal-title":"Information and Computation"},{"key":"7_CR68","volume-title":"Pitman Research Notes in Mathematics","author":"K.I. Rosenthal","year":"1990","unstructured":"Rosenthal, K.I.: Quantales and their applications. In: Pitman Research Notes in Mathematics. Longman Scientific & Technical, London (1990)"},{"key":"7_CR69","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/3-540-46419-0_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Roychoudhury","year":"2000","unstructured":"Roychoudhury, A., Narayan Kumar, K., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A.: Verification of Parameterized Systems Using Logic Program Transformations. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, pp. 172\u2013187. Springer, Heidelberg (2000)"},{"key":"7_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/978-3-540-25951-0_9","volume-title":"Program Development in Computational Logic","author":"A. Roychoudhury","year":"2004","unstructured":"Roychoudhury, A., Ramakrishnan, C.R.: Unfold\/Fold Transformations for Automated Verification of Parameterized Concurrent Systems. In: Bruynooghe, M., Lau, K.-K. (eds.) Program Development in Computational Logic. LNCS, vol.\u00a03049, pp. 261\u2013290. Springer, Heidelberg (2004)"},{"issue":"1-2","key":"7_CR71","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/S0304-3975(00)00316-9","volume":"277","author":"F. Scozzari","year":"2002","unstructured":"Scozzari, F.: Logical optimality of groundness analysis. Theor. Comput. Sci.\u00a0277(1-2), 149\u2013184 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR72","doi-asserted-by":"crossref","unstructured":"Singh, A., Ramakrishnan, C.R., Smolka, S.A.: Query-Based Model Checking of Ad Hoc Network Protocols. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol.\u00a05710, pp. 603\u2013619. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-04081-8_40"},{"issue":"1-3","key":"7_CR73","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1016\/j.tcs.2007.05.004","volume":"388","author":"F. Spoto","year":"2007","unstructured":"Spoto, F.: Optimality and condensing of information flow through linear refinement. Theor. Comput. Sci.\u00a0388(1-3), 53\u201382 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR74","first-page":"222","volume-title":"Proc. of the International Computing Symposium","author":"C. Strachey","year":"1972","unstructured":"Strachey, C.: The varieties of programming language. In: Proc. of the International Computing Symposium, Cini Foundation, Venice, pp. 222\u2013233. Springer, Heidelberg (1972)"},{"key":"7_CR75","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/3-540-45319-9_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Tan","year":"2001","unstructured":"Tan, L., Cleaveland, W.R.: Simulation revisited. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 480\u2013495. Springer, Heidelberg (2001)"},{"key":"7_CR76","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1007\/3-540-61551-2_93","volume-title":"Principles and Practice of Constraint Programming - CP\u201996","author":"L. Urbina","year":"1996","unstructured":"Urbina, L.: Analysis of Hybrid Systems in CLP(R). In: Freuder, E.C. (ed.) CP 1996. LNCS, vol.\u00a01118, pp. 451\u2013467. Springer, Heidelberg (1996)"},{"key":"7_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/11691372_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Yang","year":"2006","unstructured":"Yang, P., Basu, S., Ramakrishnan, C.R.: Parameterized Verification of \u03c0-Calculus Systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 42\u201357. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","A 25-Year Perspective on Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14309-0_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T05:32:40Z","timestamp":1740202360000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14309-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642143083","9783642143090"],"references-count":77,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14309-0_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}