{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,10]],"date-time":"2023-02-10T23:36:14Z","timestamp":1676072174863},"reference-count":69,"publisher":"Elsevier BV","issue":"1-3","license":[{"start":{"date-parts":[[1999,4,1]],"date-time":"1999-04-01T00:00:00Z","timestamp":922924800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,19]],"date-time":"2013-07-19T00:00:00Z","timestamp":1374192000000},"content-version":"vor","delay-in-days":5223,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["The Journal of Logic Programming"],"published-print":{"date-parts":[[1999,4]]},"DOI":"10.1016\/s0743-1066(98)10032-8","type":"journal-article","created":{"date-parts":[[2002,7,26]],"date-time":"2002-07-26T00:44:48Z","timestamp":1027644288000},"page":"3-42","source":"Crossref","is-referenced-by-count":3,"title":["Automated verification of Prolog programs"],"prefix":"10.1016","volume":"39","author":[{"given":"Baudouin","family":"Le Charlier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christophe","family":"Lecl\u00e8re","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sabina","family":"Rossi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Agostino","family":"Cortesi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0743-1066(98)10032-8_BIB1","series-title":"First International Static Analysis Symposium","first-page":"43","article-title":"Directional type checking of logic programs","volume":"vol. 864","author":"Aiken","year":"1994"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB2","first-page":"150","article-title":"Studies in pure prolog: Termination","volume":"volume 1","author":"Apt","year":"1990"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB3","series-title":"From Logic Programming to Prolog","author":"Apt","year":"1997"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB4","series-title":"Proceedings of the International Conference on Theoretical Aspects of Computer Science","article-title":"Proving termination of general prolog programs","author":"Apt","year":"1991"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB5","article-title":"Modular Termination of Proofs For Logic and Pure Prolog Programs","author":"Apt","year":"1993"},{"issue":"1\/2","key":"10.1016\/S0743-1066(98)10032-8_BIB6","first-page":"79","article-title":"Characterizing termination of logic programs with level mappings","volume":"15","author":"Bezem","year":"1992","journal-title":"J. Logic Programming"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB7","series-title":"Proc. ESOP'92","first-page":"73","article-title":"Typed norms","volume":"vol. 582","author":"Bossi","year":"1992"},{"issue":"2","key":"10.1016\/S0743-1066(98)10032-8_BIB8","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(92)00019-N","article-title":"Norms on terms and their use in proving universal termination of a logic program","volume":"124","author":"Bossi","year":"1994","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0743-1066(98)10032-8_BIB9","series-title":"Proceedings of the International Logic Programming Symposium (ILPS'94)","article-title":"Cardinality analysis of prolog","author":"Braem","year":"1994"},{"issue":"2","key":"10.1016\/S0743-1066(98)10032-8_BIB10","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1016\/0743-1066(91)80001-T","article-title":"A practical framework for the abstract interpretation of logic programs","volume":"10","author":"Bruynooghe","year":"1991","journal-title":"J. Logic Programming"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB11","series-title":"Computational Logic, Esprit Basic Research Series","article-title":"The synthesis of logic programs from inductive proofs","author":"Bundy","year":"1990"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB12","series-title":"Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation","first-page":"194","article-title":"Improving abstract interpretations by combining domains","author":"Codish","year":"1993"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB13","series-title":"Proceedings of the Fifth Workshop on Analysis and Verification of Multiple-Agent Languages (LOMAPS'96)","article-title":"Proving properties of logic programs by abstract diagnosis","volume":"vol. 1192","author":"Comini","year":"1996"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB14","series-title":"Logic Program Synthesis and Transformation. Proceedings of the Sixth International Workshop, LOPSTR'96","article-title":"Specification-based automatic verification of logic programs","volume":"vol. 1207","author":"Cortesi","year":"1996"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB15","article-title":"Conceptual and software support for abstract domain design: Generic structural domain and open product","author":"Cortesi","year":"1993"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB16","series-title":"Proceedings of the 21th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'94)","article-title":"Combination of abstract domains for logic programming","author":"Cortesi","year":"1994"},{"issue":"3","key":"10.1016\/S0743-1066(98)10032-8_BIB17","first-page":"237","article-title":"Type analysis of prolog using type graphs","volume":"23","author":"Cortesi","year":"1995","journal-title":"J. Logic Programming"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB18","series-title":"Conference Record of Fourth ACM Symposium on Programming Languages (POPL'77)","first-page":"238","article-title":"Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints","author":"Cousot","year":"1977"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB19","series-title":"Proceedings of the ACM Symposium on Artificial Intelligence and Programming Languages","first-page":"1","article-title":"Automatic synthesis of optimal invariant assertions: Mathematical foundation","author":"Cousot","year":"1977"},{"issue":"2\u20133","key":"10.1016\/S0743-1066(98)10032-8_BIB20","article-title":"Abstract interpretation and application to logic programs","volume":"13","author":"Cousot","year":"1992","journal-title":"J. Logic Programming"},{"issue":"4","key":"10.1016\/S0743-1066(98)10032-8_BIB21","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","article-title":"Abstract interpretation frameworks","volume":"2","author":"Cousot","year":"1992","journal-title":"J. Logic and Computation"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB22","series-title":"Inductive definitions, semantics and abstract interpretation","first-page":"83","year":"1992"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB23","series-title":"Proceedings of Programming Language Implementation and Logic Programming PLILP'90","first-page":"222","article-title":"Static type analysis of prolog procedures for ensuring correctness","volume":"vol. 456","author":"De Boeck","year":"1990"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB24","series-title":"Proceedings of LOPSTR'93, Workshops in Computer Science","article-title":"Mechanical transformation of logic definitions augmented with type information into prolog procedures: Some experiments","author":"De Boeck","year":"1993"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB25","unstructured":"D. De Schreye, S. Decorte, Termination of logic programs: The never-ending story, J. Logic Programming Special anniversary edition, accepted for publication."},{"key":"10.1016\/S0743-1066(98)10032-8_BIB26","series-title":"Proceedings of the FGCS'92","first-page":"481","article-title":"A framework for analysing the termination of definite logic programs with respect to call patterns","author":"De Schreye","year":"1992"},{"issue":"5","key":"10.1016\/S0743-1066(98)10032-8_BIB27","doi-asserted-by":"crossref","first-page":"826","DOI":"10.1145\/161468.161472","article-title":"Cost analysis of logic programs","volume":"15","author":"Debray","year":"1993","journal-title":"ACM Trans. Programming Languages and Systems"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB28","series-title":"Proceedings ACM SIGPLAN'90 conference on programming language design and implementation","first-page":"174","article-title":"Task granularity analysis in logic programs","author":"Debray","year":"1990"},{"issue":"3","key":"10.1016\/S0743-1066(98)10032-8_BIB29","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1145\/65979.65984","article-title":"Functional computations in logic programs","volume":"11","author":"Debray","year":"1989","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB30","series-title":"Technical Report","article-title":"Exploiting the power of typed norms in automatic inference of interargument relations","author":"Decorte","year":"1994"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB31","series-title":"Proceedings ILPS'93","first-page":"420","article-title":"Automatic inference of norms: A missing link in automatic termination analysis","author":"Decorte","year":"1993"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB32","series-title":"Logic Programming: Systematic Program Development","author":"Deville","year":"1990"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB33","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/0304-3975(88)90099-0","article-title":"Inductive assertion method for logic programs","volume":"59","author":"Drabent","year":"1988","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0743-1066(98)10032-8_BIB34","doi-asserted-by":"crossref","DOI":"10.1016\/S0747-7171(06)80012-X","article-title":"Logic program synthesis from incomplete specifications","author":"Flener","year":"1993","journal-title":"Journal of Symbolic Computation: Special Issue on Automatic Programming"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB35","article-title":"Program schemas as steadfast programs","author":"Flener","year":"1997"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB36","series-title":"ILPS'97 Post-Conference Workshop on Verification, Model-Checking and Abstract Interpretation","article-title":"Relating abstract interpretation with logic program verification","author":"Gallardo","year":"1997"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB37","series-title":"Proceedings of the Fourth International Workshop on Programming Language Implementation and Logic Programming (PLILP'92)","article-title":"FOLON: An environment for declarative construction of logic programs","volume":"vol. 631","author":"Henrard","year":"1992"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB38","series-title":"Proceedings of the North American Conference on Logic Programming (NACLP'89)","first-page":"154","article-title":"Accurate and efficient approximation of variable aliasing in logic programs","author":"Jacobs","year":"1989"},{"issue":"2\/3","key":"10.1016\/S0743-1066(98)10032-8_BIB39","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1016\/0743-1066(92)90032-X","article-title":"Deriving descriptions of possible values of program variables by means of abstract interpretation","volume":"13","author":"Janssens","year":"1992","journal-title":"J. Logic Programming"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB40","article-title":"Abstract equation systems: Description and insights","author":"Janssens","year":"1995"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB41","series-title":"Abstract Interpretation of Declarative Languages","first-page":"123","article-title":"A semantic-based framework for the abstract interpretation of prolog","author":"Jones","year":"1987"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB42","series-title":"Proc. Seventh Int'l Conf. on Logic Programming","first-page":"667","article-title":"Top-down synthesis of recursive logic procedures from first-order logic specifications","author":"Lau","year":"1990"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB43","doi-asserted-by":"crossref","DOI":"10.1016\/S0743-1066(98)10032-8","article-title":"Automated verification of prolog programs","author":"Le Charlier","year":"1998"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB44","article-title":"Sequence-based abstract semantics of prolog","author":"Le Charlier","year":"1996"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB45","series-title":"Proceedings of the International Logic Programming Symposium (ILPS'94)","article-title":"An abstract interpretation framework which accurately handles prolog search rule and the cut","author":"Le Charlier","year":"1994"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB46","doi-asserted-by":"crossref","DOI":"10.1017\/S1471068402001114","article-title":"Sequence-based abstract interpretation of prolog","author":"Le Charlier","year":"1997"},{"issue":"1","key":"10.1016\/S0743-1066(98)10032-8_BIB47","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1145\/174625.174627","article-title":"Experimental evaluation of a generic abstract interpretation algorithm for prolog","volume":"16","author":"Le Charlier","year":"1994","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB48","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/BF01178260","article-title":"Reexecution in abstract interpretation of prolog","volume":"32","author":"Le Charlier","year":"1995","journal-title":"Acta Informatica"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB49","article-title":"Two dual abstract operations to duplicate, eliminate, equalize, introduce and rename place-holders occurring inside abstract descriptions","author":"Lecl\u00e8re","year":"1996"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB50","series-title":"ILPS'97 Post-Conference Workshop on Verification. Model-Checking and Abstract Interpretation","article-title":"A reconstruction of verification techniques by abstract interpretation","author":"Levi","year":"1997"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB51","series-title":"Springer Series: Symbolic Computation-Artificial Intelligence","article-title":"Foundations of Logic Programming","author":"Lloyd","year":"1987"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB52","series-title":"Information Processing '89","first-page":"601","article-title":"Semantics-based dataflow analysis of logic programs","author":"Marriott","year":"1989"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB53","series-title":"Abstract Interpretation of Declarative Languages","first-page":"181","article-title":"Abstract interpretation of prolog programs","author":"Mellish","year":"1987"},{"issue":"4es","key":"10.1016\/S0743-1066(98)10032-8_BIB54","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1145\/242224.242435","article-title":"Program analysis for software engineering: New applications, new requirements, new tools","volume":"28","author":"Le M\u00e9tayer","year":"1996","journal-title":"ACM Computing Surveys"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB55","article-title":"Interpr\u00e9tation Abstraite de Programmes Prolog","author":"Musumbu","year":"1990"},{"issue":"2\/3","key":"10.1016\/S0743-1066(98)10032-8_BIB56","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1016\/0743-1066(92)90035-2","article-title":"Compile-time derivation of variable dependency using abstract interpretation","volume":"13","author":"Muthukumar","year":"1992","journal-title":"J. Logic Programming"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB57","series-title":"Proceedings of the International Workshop on Programming Language Implementation and Logic Programming (PLILP'90)","first-page":"293","article-title":"Systematic semantic approximations of logic programs","volume":"vol. 456","author":"Nilsson","year":"1990"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB58","series-title":"Proceedings ICLP'90","first-page":"634","article-title":"Termination proofs for logic programs based on predicate inequalities","author":"Pl\u00fcmer","year":"1990"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB59","series-title":"Proceedings ILPS'91","first-page":"503","article-title":"Automatic termination proofs for prolog programs operating on nonground terms","author":"Pl\u00fcmer","year":"1991"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB60","series-title":"Proceedings FGCS'92","article-title":"Automatic verification of GHC-programs: Termination","author":"Pl\u00fcmer","year":"1992"},{"issue":"1\u20133","key":"10.1016\/S0743-1066(98)10032-8_BIB61","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/S0743-1066(96)00068-4","article-title":"The execution algorithm of mercury, an efficient purely declarative logic programming language","volume":"29","author":"Somogyi","year":"1996","journal-title":"J. Logic Programming"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB62","series-title":"Proceedings of the European Symposium on Programming (ESOP'86)","first-page":"327","article-title":"An application of abstract interpretation of logic programs: Occur check reduction","volume":"vol. 213","author":"S\u00f8ndergaard","year":"1986"},{"issue":"2","key":"10.1016\/S0743-1066(98)10032-8_BIB63","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1145\/42282.42285","article-title":"Efficient tests for top-down termination of logical rules","volume":"35","author":"Ullman","year":"1988","journal-title":"J. ACM"},{"issue":"3","key":"10.1016\/S0743-1066(98)10032-8_BIB64","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1016\/0743-1066(94)00029-6","article-title":"Evaluation of Prop","volume":"23","author":"Van Hentenryck","year":"1995","journal-title":"J. Logic Programming"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB65","article-title":"Static termination analysis for definite Horn clause programs","author":"Verschaetse","year":"1992"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB66","series-title":"Proceedings ICLP'91","first-page":"301","article-title":"Deriving termination proofs for logic programs, using abstract procedures","author":"Verschaetse","year":"1991"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB67","series-title":"Proceedings LOPSTR'92","article-title":"Automatic termination analysis","volume":"vol. 883","author":"Verschaetse","year":"1993"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB68","series-title":"Proc. of the 1992 Joint International Conference and Symposium on Logic Programming","article-title":"Synthesis and transformation of logic programs in the Whelk proof development system","author":"Wiggins","year":"1992"},{"key":"10.1016\/S0743-1066(98)10032-8_BIB69","article-title":"A library for doing polyhedral operations","author":"Wilde","year":"1993"}],"container-title":["The Journal of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0743106698100328?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0743106698100328?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,16]],"date-time":"2019-04-16T14:23:15Z","timestamp":1555424595000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0743106698100328"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,4]]},"references-count":69,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[1999,4]]}},"alternative-id":["S0743106698100328"],"URL":"https:\/\/doi.org\/10.1016\/s0743-1066(98)10032-8","relation":{},"ISSN":["0743-1066"],"issn-type":[{"value":"0743-1066","type":"print"}],"subject":[],"published":{"date-parts":[[1999,4]]}}}