{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T11:02:14Z","timestamp":1740135734788,"version":"3.37.3"},"reference-count":35,"publisher":"Cambridge University Press (CUP)","issue":"3-4","license":[{"start":{"date-parts":[[2018,8,10]],"date-time":"2018-08-10T00:00:00Z","timestamp":1533859200000},"content-version":"unspecified","delay-in-days":40,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2018,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a method for automatic inference of conditions on the initial states of a program that guarantee that the safety assertions in the program are not violated. Constrained Horn clauses (CHCs) are used to model the program and assertions in a uniform way, and we use standard abstract interpretations to derive an over-approximation of the set of<jats:italic>unsafe<\/jats:italic>initial states. The precondition then is the constraint corresponding to the complement of that set, under-approximating the set of<jats:italic>safe<\/jats:italic>initial states. This idea of complementation is not new, but previous attempts to exploit it have suffered from the loss of precision. Here we develop an iterative specialisation algorithm to give more precise, and in some cases optimal safety conditions. The algorithm combines existing transformations, namely constraint specialisation, partial evaluation and a trace elimination transformation. The last two of these transformations perform polyvariant specialisation, leading to disjunctive constraints which improve precision. The algorithm is implemented and tested on a benchmark suite of programs from the literature in precondition inference and software verification competitions.<\/jats:p>","DOI":"10.1017\/s1471068418000091","type":"journal-article","created":{"date-parts":[[2018,8,10]],"date-time":"2018-08-10T05:44:17Z","timestamp":1533879857000},"page":"553-570","source":"Crossref","is-referenced-by-count":8,"title":["An iterative approach to precondition inference using constrained Horn clauses"],"prefix":"10.1017","volume":"18","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5191-1216","authenticated-orcid":false,"given":"BISHOKSAN","family":"KAFLE","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6984-7419","authenticated-orcid":false,"given":"JOHN P.","family":"GALLAGHER","sequence":"additional","affiliation":[]},{"given":"GRAEME","family":"GANGE","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5959-3769","authenticated-orcid":false,"given":"PETER","family":"SCHACHTE","sequence":"additional","affiliation":[]},{"given":"HARALD","family":"S\u00d8NDERGAARD","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2186-0459","authenticated-orcid":false,"given":"PETER J.","family":"STUCKEY","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2018,8,10]]},"reference":[{"key":"S1471068418000091_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(92)90030-7"},{"key":"S1471068418000091_ref14","first-page":"88","volume-title":"Proc. ACM SIGPLAN Symp. PEPM'93","author":"Gallagher","year":"1993"},{"key":"S1471068418000091_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"S1471068418000091_ref28","doi-asserted-by":"publisher","DOI":"10.1016\/j.cl.2015.11.001"},{"key":"S1471068418000091_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_10"},{"key":"S1471068418000091_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61580-6_7"},{"key":"S1471068418000091_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_12"},{"key":"S1471068418000091_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_43"},{"key":"S1471068418000091_ref27","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.01.002"},{"key":"S1471068418000091_ref30","doi-asserted-by":"publisher","DOI":"10.1145\/176454.176519"},{"key":"S1471068418000091_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49727-7_15"},{"key":"S1471068418000091_ref17","doi-asserted-by":"crossref","unstructured":"Grebenshchikov S. , Lopes N. P. , Popeea C. , and Rybalchenko A. 2012. Synthesizing software verifiers from proof rules. In Proc. 33rd ACM SIGPLAN Conf. Programming Language Design and Implementation, J. Vitek , H. Lin , and F. Tip , Eds. ACM, 405\u2013416.","DOI":"10.1145\/2254064.2254112"},{"volume-title":"Partial Evaluation and Automatic Software Generation","year":"1993","author":"Jones","key":"S1471068418000091_ref26"},{"key":"S1471068418000091_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_48"},{"key":"S1471068418000091_ref4","first-page":"1","volume-title":"Integrated Formal Methods","author":"Ball","year":"2004"},{"key":"S1471068418000091_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66706-5_2"},{"key":"S1471068418000091_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.05.017"},{"key":"S1471068418000091_ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78163-9_18"},{"key":"S1471068418000091_ref33","unstructured":"Min\u00e9 A. 2012b. Sufficient condition polyhedral prototype analyzer. https:\/\/www-apr.lip6.fr\/~mine\/banal\/syntax.html. Accessed: 2018-01-23."},{"key":"S1471068418000091_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2016.11.002"},{"key":"S1471068418000091_ref6","first-page":"300","volume-title":"Programming Language Design and Implementation","author":"Beyer","year":"2007"},{"key":"S1471068418000091_ref2","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1007\/978-3-319-10936-7_3","volume-title":"Static Analysis","author":"Bakhirkin","year":"2014"},{"key":"S1471068418000091_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-25951-0_6"},{"key":"S1471068418000091_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"S1471068418000091_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_33"},{"key":"S1471068418000091_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"S1471068418000091_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(98)10002-X"},{"key":"S1471068418000091_ref32","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2012.09.009"},{"key":"S1471068418000091_ref21","first-page":"219","article-title":"An overview of Ciao and its design philosophy","volume":"12","author":"Hermenegildo","year":"2012","journal-title":"TPLP"},{"key":"S1471068418000091_ref13","doi-asserted-by":"crossref","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer-Aided Verification","author":"Dutertre","year":"2014"},{"key":"S1471068418000091_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"S1471068418000091_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-67089-8_4"},{"key":"S1471068418000091_ref29","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/978-3-319-41528-4_14","volume-title":"Computer-Aided Verification","author":"Kafle","year":"2016"},{"key":"S1471068418000091_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_61"},{"key":"S1471068418000091_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_33"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068418000091","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,21]],"date-time":"2019-10-21T23:26:22Z","timestamp":1571700382000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068418000091\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7]]},"references-count":35,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2018,7]]}},"alternative-id":["S1471068418000091"],"URL":"https:\/\/doi.org\/10.1017\/s1471068418000091","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"type":"print","value":"1471-0684"},{"type":"electronic","value":"1475-3081"}],"subject":[],"published":{"date-parts":[[2018,7]]}}}