{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T10:47:27Z","timestamp":1761562047506},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662488980"},{"type":"electronic","value":"9783662488997"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-48899-7_34","type":"book-chapter","created":{"date-parts":[[2015,11,21]],"date-time":"2015-11-21T03:59:28Z","timestamp":1448078368000},"page":"483-498","source":"Crossref","is-referenced-by-count":13,"title":["Using Program Synthesis for Program Analysis"],"prefix":"10.1007","author":[{"given":"Cristina","family":"David","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]},{"given":"Matt","family":"Lewis","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,22]]},"reference":[{"key":"34_CR1","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)","DOI":"10.1145\/512950.512973"},{"key":"34_CR2","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Kroening, D., Yorav, K.: Behavioral consistency of C and verilog programs using bounded model checking. In: DAC, pp. 368\u2013371 (2003)","DOI":"10.21236\/ADA461052"},{"key":"34_CR3","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"34_CR4","doi-asserted-by":"crossref","unstructured":"Gupta, A., et al.: Proving non-termination. In: POPL (2008)","DOI":"10.1145\/1328438.1328459"},{"key":"34_CR5","unstructured":"Gulwani, S.: Dimensions in program synthesis. In: Formal Methods in Computer-Aided Design, FMCAD, p. 1 (2010)"},{"key":"34_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-642-17164-2_23","volume-title":"Programming Languages and Systems","author":"S Kong","year":"2010","unstructured":"Kong, S., Jung, Y., David, C., Wang, B.-Y., Yi, K.: Automatically inferring quantified loop invariants by algorithmic learning from simple templates. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 328\u2013343. Springer, Heidelberg (2010)"},{"key":"34_CR7","doi-asserted-by":"crossref","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: FMCAD (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"34_CR8","doi-asserted-by":"crossref","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI, pp. 405\u2013416 (2012)","DOI":"10.1145\/2345156.2254112"},{"key":"34_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"869","DOI":"10.1007\/978-3-642-39799-8_61","volume-title":"Computer Aided Verification","author":"TA Beyene","year":"2013","unstructured":"Beyene, T.A., Popeea, C., Rybalchenko, A.: Solving existentially quantified horn clauses. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 869\u2013882. Springer, Heidelberg (2013)"},{"key":"34_CR10","unstructured":"Wintersteiger, C.M., Hamadi, Y., de Moura, L.M.: Efficiently solving quantified bit-vector formulas. In: FMCAD (2010)"},{"issue":"4","key":"34_CR11","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/s10817-009-9161-6","volume":"44","author":"R Piskac","year":"2010","unstructured":"Piskac, R., de Moura, L.M., Bj\u00f8rner, N.: Deciding effectively propositional logic using DPLL and substitution sets. J. Autom. Reasoning 44(4), 401\u2013424 (2010)","journal-title":"J. Autom. Reasoning"},{"key":"34_CR12","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: PLDI, pp. 281\u2013292 (2008)","DOI":"10.1145\/1379022.1375616"},{"key":"34_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-662-46669-8_8","volume-title":"Programming Languages and Systems","author":"C David","year":"2015","unstructured":"David, C., Kroening, D., Lewis, M.: Unrestricted termination and non-termination arguments for bit-vector programs. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 183\u2013204. Springer, Heidelberg (2015)"},{"key":"34_CR14","doi-asserted-by":"crossref","unstructured":"David, C., Kroening, D., Lewis, M.: Using program synthesis for program analysis. CoRR abs\/1508.07829 (2015)","DOI":"10.1007\/978-3-662-48899-7_34"},{"issue":"5\u20136","key":"34_CR15","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/s10009-012-0249-7","volume":"15","author":"A Solar-Lezama","year":"2013","unstructured":"Solar-Lezama, A.: Program sketching. STTT 15(5\u20136), 475\u2013495 (2013)","journal-title":"STTT"},{"key":"34_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/11799573_21","volume-title":"Logic Programming","author":"M Brain","year":"2006","unstructured":"Brain, M., Crick, T., De Vos, M., Fitch, J.: TOAST: applying answer set programming to superoptimisation. In: Etalle, S., Truszczy\u0144ski, M. (eds.) ICLP 2006. LNCS, vol. 4079, pp. 270\u2013284. Springer, Heidelberg (2006)"},{"key":"34_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-04726-2","volume-title":"Foundations of Genetic Programming","author":"WB Langdon","year":"2002","unstructured":"Langdon, W.B., Poli, R.: Foundations of Genetic Programming. Springer, Heidelberg (2002)"},{"key":"34_CR18","volume-title":"Linear Genetic Programming","author":"M Brameier","year":"2007","unstructured":"Brameier, M., Banzhaf, W.: Linear Genetic Programming. Springer, Heidelberg (2007)"},{"key":"34_CR19","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1177\/105971239700500305","volume":"5","author":"F Gomez","year":"1997","unstructured":"Gomez, F., Miikkulainen, R.: Incremental evolution of complex general behavior. Adapt. Behav. 5, 317\u2013342 (1997)","journal-title":"Adapt. Behav."},{"key":"34_CR20","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: PLDI, pp. 62\u201373 (2011)","DOI":"10.1145\/1993316.1993506"},{"key":"34_CR21","unstructured":"SV-COMP. \n                    http:\/\/sv-comp.sosy-lab.org\/2015\/"},{"key":"34_CR22","doi-asserted-by":"crossref","unstructured":"David, C., Kroening, D., Lewis, M.: Danger invariants. CoRR (2015)","DOI":"10.1007\/978-3-319-48989-6_12"},{"key":"34_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-319-21668-3_12","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2015","unstructured":"Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., Barrett, C.: Counterexample-guided quantifier instantiation for synthesis in SMT. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 198\u2013216. Springer, Heidelberg (2015)"},{"key":"34_CR24","unstructured":"StarExec. \n                    https:\/\/www.starexec.org"},{"key":"34_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/978-3-319-08867-9_5","volume-title":"Computer Aided Verification","author":"P Garg","year":"2014","unstructured":"Garg, P., L\u00f6ding, C., Madhusudan, P., Neider, D.: ICE:\u00a0a\u00a0robust\u00a0framework\u00a0for\u00a0learning\u00a0invariants. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 69\u201387. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48899-7_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T19:25:49Z","timestamp":1559330749000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-48899-7_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662488980","9783662488997"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48899-7_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}