{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:34:53Z","timestamp":1750221293008,"version":"3.41.0"},"reference-count":83,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2018,5,28]],"date-time":"2018-05-28T00:00:00Z","timestamp":1527465600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/H017585\/1"],"award-info":[{"award-number":["EP\/H017585\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"name":"H2020 FET OPEN project","award":["712689 SC2"],"award-info":[{"award-number":["712689 SC2"]}]},{"name":"ERC","award":["280053 CPROVER"],"award-info":[{"award-number":["280053 CPROVER"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2018,6,30]]},"abstract":"<jats:p>\n            In this article, we propose a\n            <jats:italic>unified<\/jats:italic>\n            framework for designing static analysers based on\n            <jats:italic>program synthesis<\/jats:italic>\n            . For this purpose, we identify a fragment of second-order logic with restricted quantification that is expressive enough to model numerous static analysis problems (e.g., safety proving, bug finding, termination and non-termination proving, refactoring). As our focus is on programs that use bit-vectors, we build a decision procedure for this fragment over finite domains in the form of a program synthesiser. We\u00a0provide instantiations of our framework for solving a diverse range of program verification tasks such as termination, non-termination, safety and bug finding, superoptimisation, and refactoring. Our experimental results show that our program synthesiser compares positively with specialised tools in each area as well as with general-purpose synthesisers.\n          <\/jats:p>","DOI":"10.1145\/3174802","type":"journal-article","created":{"date-parts":[[2018,5,29]],"date-time":"2018-05-29T12:24:26Z","timestamp":1527596666000},"page":"1-45","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Program Synthesis for Program Analysis"],"prefix":"10.1145","volume":"40","author":[{"given":"Cristina","family":"David","sequence":"first","affiliation":[{"name":"University of Oxford, UK"}]},{"given":"Pascal","family":"Kesseli","sequence":"additional","affiliation":[{"name":"University of Oxford, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6681-5283","authenticated-orcid":false,"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[{"name":"University of Oxford, UK"}]},{"given":"Matt","family":"Lewis","sequence":"additional","affiliation":[{"name":"University of Oxford, UK"}]}],"member":"320","published-online":{"date-parts":[[2018,5,28]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3049797.3049802"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_23"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/1816978"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/78995"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11737414_14"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_11"},{"key":"e_1_2_2_9_1","volume-title":"Size-change termination, monotonicity constraints and ranking functions. Logical Methods in Computer Science 6, 3","author":"Ben-Amram Amir M.","year":"2010","unstructured":"Amir M. Ben-Amram. 2010. Size-change termination, monotonicity constraints and ranking functions. Logical Methods in Computer Science 6, 3 (2010)."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429078"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2632362.2632364"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_61"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032321"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_48"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_109"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_8"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11799573_21"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","unstructured":"M. F. Brameier and W. Banzhaf. 2007. Linear Genetic Programming. Springer.","DOI":"10.5555\/1951880"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_28"},{"volume-title":"Proving Nontermination via Safety","author":"Chen Hong-Yi","key":"e_1_2_2_20_1","unstructured":"Hong-Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, and Peter O\u2019Hearn. 2014. Proving Nontermination via Safety. Springer, 156--171."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_28"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462180"},{"key":"e_1_2_2_23_1","volume-title":"Proceedings of the International Congress of Mathematicians. 23--35","author":"Church Alonzo","year":"1962","unstructured":"Alonzo Church. 1962. Logic, arithmetic, automata. In Proceedings of the International Congress of Mathematicians. 23--35."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775928"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"e_1_2_2_27_1","volume-title":"Proceedings of the 13th Workshop on Logic Programming Environments. 48--59","author":"Codish Michael","year":"2003","unstructured":"Michael Codish and Samir Genaim. 2003. Proving termination one loop at a time. In Proceedings of the 13th Workshop on Logic Programming Environments. 48--59."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_19"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_4"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_32_1","volume-title":"Kayak: Safe Semantic Refactoring to Java Streams. Technical Report","author":"David Cristina","year":"2016","unstructured":"Cristina David, Pascal Kesseli, and Daniel Kroening. 2016. Kayak: Safe Semantic Refactoring to Java Streams. Technical Report. University of Oxford. https:\/\/www.cs.ox.ac.uk\/files\/9156\/stream-extended.pdf."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_12"},{"key":"e_1_2_2_34_1","doi-asserted-by":"crossref","unstructured":"Cristina David and Daniel Kroening. 2017. Program synthesis: Challenges and opportunities. In Philosophical Transactions of the Royal Society A. To appear.","DOI":"10.1098\/rsta.2015.0403"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_8"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_34"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_35"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s002000100065"},{"key":"e_1_2_2_39_1","unstructured":"Ronald Fagin. 1974. Generalized first-order spectra and polynomial-time recognizable sets. In Complexity of Computation R. Karp (Ed.)."},{"volume-title":"Assigning Meanings to Programs","author":"Floyd Robert W.","key":"e_1_2_2_40_1","unstructured":"Robert W. Floyd. 1993. Assigning Meanings to Programs. Springer, Dordrecht, Netherlands, 65--81."},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/559915"},{"key":"e_1_2_2_42_1","volume-title":"ICE: A Robust Framework for Learning Invariants","author":"Garg Pranav","year":"2014","unstructured":"Pranav Garg, Christof L\u00f6ding, P. Madhusudan, and Daniel Neider. 2014. ICE: A Robust Framework for Learning Invariants. Springer International Publishing, Cham, 69--87."},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/1880443.1880451"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1177\/105971239700500305"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254112"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1836089.1836091"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542518"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993506"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375616"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328897.1328459"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_41"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_42"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/1882094.1882113"},{"volume-title":"Linear Ranking for Linear Lasso Programs","author":"Heizmann Matthias","key":"e_1_2_2_54_1","unstructured":"Matthias Heizmann, Jochen Hoenicke, Jan Leike, and Andreas Podelski. 2013. Linear Ranking for Linear Lasso Programs. Springer International Publishing, Cham, 365--380."},{"key":"e_1_2_2_55_1","volume-title":"Jie-Hong Roland Jiang, and Roderick Bloem","author":"Hofferek Georg","year":"2013","unstructured":"Georg Hofferek, Ashutosh Gupta, Bettina K\u00f6nighofer, Jie-Hong Roland Jiang, and Roderick Bloem. 2013. Synthesizing multiple Boolean functions using interpolation on a single proof. http:\/\/arxiv.org\/abs\/1308.4767, CoRR abs\/1308.4767."},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11970-5_6"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806833"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/9.618239"},{"key":"e_1_2_2_59_1","volume-title":"Proceedings of the American Control Conference","volume":"5","author":"Lee","unstructured":"Lee H. Keel and Shankar P. Bhattacharyya. 1998. Stability margins and digital implementation of controllers. In Proceedings of the American Control Conference, Vol. 5. 2852--2856."},{"volume-title":"Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates","author":"Kong Soonho","key":"e_1_2_2_60_1","unstructured":"Soonho Kong, Yungbum Jung, Cristina David, Bow-Yaw Wang, and Kwangkeun Yi. 2010. Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates. Springer, 328--343."},{"key":"e_1_2_2_61_1","doi-asserted-by":"crossref","unstructured":"Ina Kraan David Basin and Alan Bundy. 1993. Logic program synthesis via proof planning. In Logic Program Synthesis and Transformation. 1--14.","DOI":"10.1007\/978-1-4471-3560-9_1"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_26"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19249-9_21"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_9"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.5555\/1965360"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679413"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/362566.362568"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806852"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491413"},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021840"},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.5555\/1855676.1855683"},{"volume-title":"Counterexample-Guided Quantifier Instantiation for Synthesis in SMT","author":"Reynolds Andrew","key":"e_1_2_2_74_1","unstructured":"Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, and Clark Barrett. 2015. Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. Springer International Publishing, Cham, 198--216."},{"key":"e_1_2_2_75_1","volume-title":"Retrieved","author":"Rybalchenko Andrey","year":"2014","unstructured":"Andrey Rybalchenko. 2011. ARMC. Retrieved November 2014 from http:\/\/www7.in.tum.de\/rybal\/armc."},{"key":"e_1_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_2_2_77_1","volume-title":"Retrieved","author":"SV-COMP.","year":"2014","unstructured":"SV-COMP. 2015. Retrieved November 2014 from http:\/\/sv-comp.sosy-lab.org\/2015\/."},{"key":"e_1_2_2_78_1","volume-title":"Retrieved","author":"SV-COMP.","year":"2015","unstructured":"SV-COMP. 2016. Retrieved November 2015 from http:\/\/sv-comp.sosy-lab.org\/2016\/."},{"key":"e_1_2_2_79_1","first-page":"230","article-title":"On computable numbers with an application to the Entscheidungsproblem","volume":"2","author":"Turing Alan","year":"1936","unstructured":"Alan Turing. 1936. On computable numbers with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society 2 (1936), 230\u2013265.","journal-title":"Proceedings of the London Mathematical Society"},{"key":"e_1_2_2_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_5"},{"key":"e_1_2_2_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/2883817.2883824"},{"volume-title":"Addison-Wesley Longman Publishing Co","author":"Warren Henry S.","key":"e_1_2_2_82_1","unstructured":"Henry S. Warren. 2002. Hacker\u2019s Delight. Addison-Wesley Longman Publishing Co., Inc., Boston, MA."},{"key":"e_1_2_2_83_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0156-2"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3174802","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3174802","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:33Z","timestamp":1750212693000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3174802"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,5,28]]},"references-count":83,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,6,30]]}},"alternative-id":["10.1145\/3174802"],"URL":"https:\/\/doi.org\/10.1145\/3174802","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2018,5,28]]},"assertion":[{"value":"2016-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-12-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-05-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}