{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T13:26:33Z","timestamp":1751635593396,"version":"3.40.5"},"reference-count":42,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2021,9,23]],"date-time":"2021-09-23T00:00:00Z","timestamp":1632355200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2021,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Precondition inference is a non-trivial problem with important applications in program analysis and verification. We present a novel iterative method for automatically deriving preconditions for the safety and unsafety of programs. Each iteration maintains over-approximations of the set of <jats:italic>safe<\/jats:italic> and <jats:italic>unsafe initial<\/jats:italic> states, which are used to partition the program\u2019s <jats:italic>initial<\/jats:italic> states into those known to be <jats:italic>safe<\/jats:italic>, known to be <jats:italic>unsafe<\/jats:italic> and <jats:italic>unknown<\/jats:italic>. We then construct revised programs with those <jats:italic>unknown<\/jats:italic> initial states and iterate the procedure until the approximations are disjoint or some termination criteria are met. An experimental evaluation of the method on a set of software verification benchmarks shows that it can infer precise preconditions (sometimes optimal) that are not possible using previous methods.<\/jats:p>","DOI":"10.1017\/s1471068421000272","type":"journal-article","created":{"date-parts":[[2021,9,23]],"date-time":"2021-09-23T13:05:58Z","timestamp":1632402358000},"page":"700-716","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":3,"title":["Transformation-Enabled Precondition Inference"],"prefix":"10.1017","volume":"21","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5191-1216","authenticated-orcid":false,"given":"BISHOKSAN","family":"KAFLE","sequence":"first","affiliation":[]},{"given":"GRAEME","family":"GANGE","sequence":"additional","affiliation":[]},{"given":"PETER J.","family":"STUCKEY","sequence":"additional","affiliation":[]},{"given":"PETER","family":"SCHACHTE","sequence":"additional","affiliation":[]},{"given":"HARALD","family":"S\u00d8NDERGAARD","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2021,9,23]]},"reference":[{"key":"S1471068421000272_ref25","doi-asserted-by":"crossref","unstructured":"Howe, J. M. , King, A. and Lu, L. 2004. Analysing logic programs by reasoning backwards. In Program Development in Computational Logic. LNCS, vol. 3049. Springer, 152\u2013188.","DOI":"10.1007\/978-3-540-25951-0_6"},{"key":"S1471068421000272_ref3","doi-asserted-by":"crossref","unstructured":"Bakhirkin, A. and Monniaux, D. 2017. Combining forward and backward abstract interpretation of Horn clauses. In SAS 2017. LNCS, vol. 10422. Springer, 23\u201345.","DOI":"10.1007\/978-3-319-66706-5_2"},{"key":"S1471068421000272_ref23","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A. , Kahsai, T. , Komuravelli, A. and Navas, J. A. 2015. The SeaHorn verification framework. In CAV 2015. LNCS, vol. 9206. Springer, 343\u2013361.","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"S1471068421000272_ref36","unstructured":"Muthukumar, K. and Hermenegildo, M. 1990. Deriving a Fixpoint Computation Algorithm for Top-down Abstract Interpretation of Logic Programs. Technical Report ACT-DC-153-90, Microelectronics and Computer Technology Corporation (MCC), Austin, TX 78759. April."},{"key":"S1471068421000272_ref22","doi-asserted-by":"crossref","unstructured":"Gupta, A. and Rybalchenko, A. 2009. Invgen: An efficient invariant generator. In CAV, Bouajjani, A. and Maler, O. , Eds. LNCS, vol. 5643. Springer, 634\u2013640.","DOI":"10.1007\/978-3-642-02658-4_48"},{"key":"S1471068421000272_ref13","doi-asserted-by":"crossref","unstructured":"De Angelis, E. , Fioravanti, F. , Pettorossi, A. and Proietti, M. 2017. Semantics-based generation of verification conditions via program specialization. Science of Computer Programming 147, 78\u2013108.","DOI":"10.1016\/j.scico.2016.11.002"},{"key":"S1471068421000272_ref26","doi-asserted-by":"crossref","unstructured":"Jaffar, J. , Murali, V. , Navas, J. A. and Santosa, A. E. 2012. TRACER: A symbolic execution tool for verification. In CAV 2012. LNCS, vol. 7358. Springer, 758\u2013766.","DOI":"10.1007\/978-3-642-31424-7_61"},{"key":"S1471068421000272_ref32","doi-asserted-by":"publisher","DOI":"10.1145\/176454.176519"},{"key":"S1471068421000272_ref14","doi-asserted-by":"crossref","unstructured":"Dillig, I. , Dillig, T. , Li, B. and McMillan, K. L. 2013. Inductive invariant generation via abductive inference. In OOPSLA 2013. ACM, 443\u2013456.","DOI":"10.1145\/2509136.2509511"},{"volume-title":"Partial Evaluation and Automatic Software Generation","year":"1993","author":"Jones","key":"S1471068421000272_ref27"},{"key":"S1471068421000272_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"S1471068421000272_ref17","doi-asserted-by":"crossref","unstructured":"Gallagher, J. P. 2019. Polyvariant program specialisation with property-based abstraction. In VPT 2019. EPTCS, vol. 299. 34\u201348.","DOI":"10.4204\/EPTCS.299.6"},{"key":"S1471068421000272_ref24","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000457"},{"key":"S1471068421000272_ref30","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068418000091"},{"key":"S1471068421000272_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/j.cl.2015.11.001"},{"key":"S1471068421000272_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.05.017"},{"key":"S1471068421000272_ref10","doi-asserted-by":"crossref","unstructured":"Cousot, P. and Halbwachs, N. 1978. Automatic discovery of linear restraints among variables of a program. In POPL. ACM Press, 84\u201396.","DOI":"10.1145\/512760.512770"},{"key":"S1471068421000272_ref38","doi-asserted-by":"crossref","unstructured":"Peralta, J. C. , Gallagher, J. P. and Sa\u011flam, H. 1998. Analysis of imperative programs through analysis of constraint logic programs. In SAS 1998. LNCS, vol. 1503. 246\u2013261.","DOI":"10.1007\/3-540-49727-7_15"},{"key":"S1471068421000272_ref39","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2012.07.004"},{"key":"S1471068421000272_ref12","doi-asserted-by":"crossref","unstructured":"De Angelis, E. , Fioravanti, F. , Pettorossi, A. and Proietti, M. 2014. VeriMAP: A tool for verifying programs through transformations. In TACAS 2014. LNCS, vol. 8413. Springer, 568\u2013574.","DOI":"10.1007\/978-3-642-54862-8_47"},{"key":"S1471068421000272_ref35","doi-asserted-by":"crossref","unstructured":"Moy, Y. 2008. Sufficient preconditions for modular assertion checking. In VMCAI 2008. LNCS, vol. 4905. Springer, 188\u2013202.","DOI":"10.1007\/978-3-540-78163-9_18"},{"key":"S1471068421000272_ref2","doi-asserted-by":"crossref","unstructured":"Bakhirkin, A. , Berdine, J. and Piterman, N. 2014. Backward analysis via over-approximate abstraction and under-approximate subtraction. In SAS 2014. LNCS, vol. 8723. Springer, 34\u201350.","DOI":"10.1007\/978-3-319-10936-7_3"},{"key":"S1471068421000272_ref42","doi-asserted-by":"crossref","unstructured":"Seghir, M. N. and Schrammel, P. 2014. Necessary and sufficient preconditions via eager abstraction. In APLAS 2014. LNCS, vol. 8858. Springer, 236\u2013254.","DOI":"10.1007\/978-3-319-12736-1_13"},{"key":"S1471068421000272_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"S1471068421000272_ref6","doi-asserted-by":"crossref","unstructured":"Cassez, F. , Jensen, P. G. and Larsen, K. G. 2017. Refinement of trace abstraction for real-time programs. In Reachability Problems. LNCS, vol. 10506. Springer, 42\u201358.","DOI":"10.1007\/978-3-319-67089-8_4"},{"key":"S1471068421000272_ref9","doi-asserted-by":"crossref","unstructured":"Cousot, P. , Cousot, R. , F\u00e4hndrich, M. and Logozzo, F. 2013. Automatic inference of necessary preconditions. In VMCAI\u201913. LNCS, vol. 7737. Springer, 128\u2013148.","DOI":"10.1007\/978-3-642-35873-9_10"},{"key":"S1471068421000272_ref37","doi-asserted-by":"crossref","unstructured":"Padhi, S. , Sharma, R. and Millstein, T. D. 2016. Data-driven precondition inference with learned features. In PLDI 2016. ACM, 42\u201356.","DOI":"10.1145\/2980983.2908099"},{"key":"S1471068421000272_ref40","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(99)00031-X"},{"key":"S1471068421000272_ref4","doi-asserted-by":"crossref","unstructured":"Beyer, D. 2021. Software verification: 10th comparative evaluation (SV-COMP 2021). In TACAS 2021, Groote, J. F. and Larsen, K. G. , Eds. LNCS. Springer, 401\u2013422.","DOI":"10.1007\/978-3-030-72013-1_24"},{"key":"S1471068421000272_ref8","doi-asserted-by":"crossref","unstructured":"Cousot, P. and Cousot, R. 1992. Abstract interpretation and application to logic programs. J. Logic Programming 13, 2&3, 103\u2013179.","DOI":"10.1016\/0743-1066(92)90030-7"},{"key":"S1471068421000272_ref20","doi-asserted-by":"crossref","unstructured":"Gulavani, B. S. , Chakraborty, S. , Nori, A. V. and Rajamani, S. K. 2008. Automatically refining abstract interpretations. In TACAS 2008. LNCS, vol. 4963. Springer, 443\u2013458.","DOI":"10.1007\/978-3-540-78800-3_33"},{"key":"S1471068421000272_ref21","doi-asserted-by":"crossref","unstructured":"Gulwani, S. , Jain, S. and Koskinen, E. 2009. Control-flow refinement and progress invariants for bound analysis. In PLDI. ACM, 375\u2013385.","DOI":"10.1145\/1543135.1542518"},{"key":"S1471068421000272_ref34","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2012.09.009"},{"key":"S1471068421000272_ref5","doi-asserted-by":"crossref","unstructured":"Beyer, D. , Henzinger, T. A. , Majumdar, R. and Rybalchenko, A. 2007. Path invariants. In PLDI, Ferrante, J. and McKinley, K. S. , Eds. ACM, 300\u2013309.","DOI":"10.1145\/1273442.1250769"},{"key":"S1471068421000272_ref41","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S. , Sipma, H. and Manna, Z. 2004. Non-linear loop invariant generation using Gr\u00f6bner bases. In POPL. ACM, 318\u2013329.","DOI":"10.1145\/982962.964028"},{"key":"S1471068421000272_ref16","doi-asserted-by":"crossref","unstructured":"Dutertre, B. 2014. Yices 2.2. In CAV 2014. LNCS, vol. 8559. Springer, 737\u2013744.","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"S1471068421000272_ref18","doi-asserted-by":"crossref","unstructured":"Gallagher, J. P. and Lafave, L. 1996. Regular approximation of computation paths in logic and functional languages. In Partial Evaluation. LNCS, vol. 1110. Springer, 115\u2013136.","DOI":"10.1007\/3-540-61580-6_7"},{"key":"S1471068421000272_ref19","doi-asserted-by":"crossref","unstructured":"Grebenshchikov, S. , Lopes, N. P. , Popeea, C. and Rybalchenko, A. 2012. Synthesizing software verifiers from proof rules. In PLDI 2012. ACM, 405\u2013416.","DOI":"10.1145\/2345156.2254112"},{"key":"S1471068421000272_ref7","doi-asserted-by":"crossref","unstructured":"Codish, M. and S\u00f8ndergaard, H. 2002. Meta-circular abstract interpretation in Prolog. In The Essence of Computation, T. Mogensen et al., Eds. LNCS, vol. 2566. Springer, 109\u2013134.","DOI":"10.1007\/3-540-36377-7_6"},{"key":"S1471068421000272_ref28","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.01.002"},{"key":"S1471068421000272_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268497"},{"key":"S1471068421000272_ref15","doi-asserted-by":"crossref","unstructured":"Dom\u00e9nech, J. J. , Gallagher, J. P. and Genaim, S. 2019. Control-flow refinement by partial evaluation, and its application to termination and cost analysis. Theory and Practice of Logic Programming 19, 5\u20136, 990\u20131005.","DOI":"10.1017\/S1471068419000310"}],"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\/S1471068421000272","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T10:17:59Z","timestamp":1641464279000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068421000272\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,23]]},"references-count":42,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2021,11]]}},"alternative-id":["S1471068421000272"],"URL":"https:\/\/doi.org\/10.1017\/s1471068421000272","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"type":"print","value":"1471-0684"},{"type":"electronic","value":"1475-3081"}],"subject":[],"published":{"date-parts":[[2021,9,23]]},"assertion":[{"value":"\u00a9 The Author(s), 2021. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}