{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T06:56:12Z","timestamp":1772175372947,"version":"3.50.1"},"reference-count":64,"publisher":"Springer Science and Business Media LLC","issue":"5-6","license":[{"start":{"date-parts":[[2012,1,25]],"date-time":"2012-01-25T00:00:00Z","timestamp":1327449600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2013,10]]},"DOI":"10.1007\/s10009-012-0223-4","type":"journal-article","created":{"date-parts":[[2012,1,24]],"date-time":"2012-01-24T19:37:07Z","timestamp":1327433827000},"page":"497-518","source":"Crossref","is-referenced-by-count":66,"title":["Template-based program verification and program synthesis"],"prefix":"10.1007","volume":"15","author":[{"given":"Saurabh","family":"Srivastava","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sumit","family":"Gulwani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeffrey S.","family":"Foster","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,1,25]]},"reference":[{"key":"223_CR1","doi-asserted-by":"crossref","unstructured":"Bauer, F.L., Ehler, H., Horsch, A., Moeller, B., Partsch, H., Paukner, O., Pepper, P.: The\/Munich project CIP (1988)","DOI":"10.1007\/3-540-18779-0"},{"key":"223_CR2","unstructured":"Beucher, O.: MATLAB und simulink (scientific computing). Pearson Studium, 08 (2006)"},{"key":"223_CR3","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T. Majumdar, R., Rybalchenko, A.: Path invariants. In: PLDI (2007)","DOI":"10.1145\/1250734.1250769"},{"key":"223_CR4","doi-asserted-by":"crossref","unstructured":"Col\u00f3n, M.: Schema-guided synthesis of imperative programs by constraint solving. In: LOPSTR, pp. 166\u2013181. (2004)","DOI":"10.1007\/11506676_11"},{"key":"223_CR5","doi-asserted-by":"crossref","unstructured":"Col\u00f3n, M., Sankaranarayanan, S., Sipma, H.: Linear invariant generation using non-linear constraint solving. In: CAV, pp. 420\u2013432. (2003)","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"223_CR6","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R.L. Constable","year":"1986","unstructured":"Constable R.L.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Upper Saddle River, NJ (1986)"},{"key":"223_CR7","doi-asserted-by":"crossref","unstructured":"Cook, B., Gupta, A., Magill, S., Rybalchenko, A., Simsa, J., Singh, S., Vafeiadis, V.: Finding heap-bounds for hardware synthesis. In: FMCAD, pp. 205\u2013212. (2009)","DOI":"10.1109\/FMCAD.2009.5351120"},{"key":"223_CR8","volume-title":"Introduction to Algorithms","author":"T. Cormen","year":"1990","unstructured":"Cormen T., Leiserson C., Rivest R.: Introduction to Algorithms. The MIT Press, Cambridge, MA (1990)"},{"key":"223_CR9","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, pp. 238\u2013252. (1977)","DOI":"10.1145\/512950.512973"},{"issue":"2&3","key":"223_CR10","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/0743-1066(92)90030-7","volume":"13","author":"P. Cousot","year":"1992","unstructured":"Cousot P., Cousot R.: Abstract interpretation and application to logic programs. J. Log. Program. 13(2&3), 103\u2013179 (1992)","journal-title":"J. Log. Program."},{"key":"223_CR11","doi-asserted-by":"crossref","unstructured":"Das, S., Dill, D.L.: Counter-example based predicate discovery in predicate abstraction. In: FMCAD, pp. 19\u201332. (2002)","DOI":"10.1007\/3-540-36126-X_2"},{"key":"223_CR12","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Efficient E-matching for smt solvers. In: CADE-21, pp. 183\u2013198. (2007)","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"223_CR13","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3. http:\/\/research.microsoft.com\/projects\/Z3\/ (2008)"},{"key":"223_CR14","unstructured":"Denney, E.: A theory of program refinement. PhD thesis, University of Edinburgh (1999)"},{"key":"223_CR15","doi-asserted-by":"crossref","unstructured":"Duran, J.W.: Heuristics for program synthesis using loop invariants. In: ACM, pp. 891\u2013900. (1978)","DOI":"10.1145\/800178.810159"},{"key":"223_CR16","doi-asserted-by":"crossref","unstructured":"Emerson, T., Burstein, M.H.: Development of a constraint-based airlift scheduler by program synthesis from formal specifications. In: ASE, p. 267. (1999)","DOI":"10.1109\/ASE.1999.802313"},{"issue":"3","key":"223_CR17","doi-asserted-by":"crossref","first-page":"483","DOI":"10.1017\/S0956796802004562","volume":"13","author":"B. Fischer","year":"2003","unstructured":"Fischer B., Schumann J.: Autobayes: a system for generating data analysis programs from statistical models. J. Funct. Program. 13(3), 483\u2013508 (2003)","journal-title":"J. Funct. Program."},{"key":"223_CR18","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL, pp. 191\u2013202. (2002)","DOI":"10.1145\/565816.503291"},{"issue":"1","key":"223_CR19","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1006\/jsco.1999.0348","volume":"30","author":"P. Flener","year":"2000","unstructured":"Flener P., Lau K.-K., Ornaghi M., Richardson J.: An abstract formalization of correct schemas for program synthesis. J. Symb. Comput. 30(1), 93\u2013127 (2000)","journal-title":"J. Symb. Comput."},{"key":"223_CR20","doi-asserted-by":"crossref","unstructured":"Gopan, D., Reps, T.W.: Lookahead widening. In: CAV, pp. 452\u2013466. (2006)","DOI":"10.1007\/11817963_41"},{"key":"223_CR21","doi-asserted-by":"crossref","unstructured":"Gopan, D., Reps, T.W.: Guided static analysis. In: SAS, pp. 349\u2013365. (2007)","DOI":"10.1007\/978-3-540-74061-2_22"},{"key":"223_CR22","doi-asserted-by":"crossref","unstructured":"Green, C.: Application of theorem proving to problem solving. In: IJCAI, pp. 219\u2013239. (1969)","DOI":"10.21236\/ADA459656"},{"key":"223_CR23","doi-asserted-by":"crossref","unstructured":"Gulwani, S.: Dimensions in program synthesis. In: FMCAD, p. 1. (2010)","DOI":"10.1145\/1836089.1836091"},{"key":"223_CR24","doi-asserted-by":"crossref","unstructured":"Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: POPL, pp. 317\u2013330. (2011)","DOI":"10.1145\/1925844.1926423"},{"key":"223_CR25","unstructured":"Gulavani, B.S., Chakraborty, S., Nori, A.V., Rajamani, S.K.: Automatically refining abstract interpretations. TR-07-23 (2007)"},{"key":"223_CR26","doi-asserted-by":"crossref","unstructured":"Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: POPL, pp. 235\u2013246. (2008)","DOI":"10.1145\/1328897.1328468"},{"key":"223_CR27","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: PLDI. (2008)","DOI":"10.1145\/1375581.1375616"},{"key":"223_CR28","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Constraint-based invariant inference over predicate abstraction. In: VMCAI (2009)","DOI":"10.1007\/978-3-540-93900-9_13"},{"key":"223_CR29","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":"223_CR30","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Korthikanti, V.A., Tiwari, A.: Synthesizing geometry constructions. In: PLDI, pp. 50\u201361. (2011)","DOI":"10.1145\/1993316.1993505"},{"key":"223_CR31","doi-asserted-by":"crossref","unstructured":"Gupta, A., Majumdar, R., Rybalchenko, A.: From tests to proofs. In: TACAS, pp. 262\u2013276. (2009)","DOI":"10.1007\/978-3-642-00768-2_24"},{"key":"223_CR32","doi-asserted-by":"crossref","unstructured":"Gupta, A., Rybalchenko, A.: Invgen: an efficient invariant generator. In: CAV, pp. 634\u2013640. (2009)","DOI":"10.1007\/978-3-642-02658-4_48"},{"key":"223_CR33","doi-asserted-by":"crossref","unstructured":"Harris, W.R., Gulwani, S.: Spreadsheet table transformations from examples. In: PLDI, pp. 317\u2013328. (2011)","DOI":"10.1145\/1993316.1993536"},{"key":"223_CR34","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL, pp. 232\u2013244. (2004)","DOI":"10.1145\/982962.964021"},{"key":"223_CR35","doi-asserted-by":"crossref","unstructured":"Itzhaky, S., Gulwani, S., Immerman, N., Sagiv, M.: A simple inductive synthesis methodology and its applications. In: OOPSLA, pp. 36\u201346. (2010)","DOI":"10.1145\/1932682.1869463"},{"key":"223_CR36","doi-asserted-by":"crossref","unstructured":"Jha, S., Gulwani, S., Seshia, S., Tiwari, A.: Oracle-guided component-based program synthesis. In: ICSE (2010)","DOI":"10.1145\/1806799.1806833"},{"key":"223_CR37","doi-asserted-by":"crossref","unstructured":"Jhala, R., McMillan, K.: Array abstractions from proofs. In: CAV (2007)","DOI":"10.1007\/978-3-540-73368-3_23"},{"key":"223_CR38","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1016\/S0304-3975(96)00163-6","volume":"173","author":"S. Kahrs","year":"1997","unstructured":"Kahrs S., Sannella D., Tarlecki A.: The definition of extended ML: a gentle introduction. Theor. Comput. Sci. 173, 445\u2013484 (1997)","journal-title":"Theor. Comput. Sci."},{"key":"223_CR39","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: PLDI (2010)","DOI":"10.1145\/1806596.1806632"},{"key":"223_CR40","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Bryant, R.E.: Constructing quantified invariants via predicate abstraction. In: VMCAI, pp. 331\u2013353. (2004)","DOI":"10.1007\/978-3-540-24622-0_22"},{"key":"223_CR41","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Bryant, R.E.: Indexed predicate discovery for unbounded system verification. In: CAV, pp. 135\u2013147. (2004)","DOI":"10.1007\/978-3-540-27813-9_11"},{"issue":"1","key":"223_CR42","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1145\/1297658.1297662","volume":"9","author":"S.K. Lahiri","year":"2007","unstructured":"Lahiri S.K., Bryant R.E.: Predicate abstraction with indexed predicates. ACM Trans. Comput. Log. 9(1), 4 (2007)","journal-title":"ACM Trans. Comput. Log."},{"issue":"3","key":"223_CR43","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/362566.362568","volume":"14","author":"Z. Manna","year":"1971","unstructured":"Manna Z., Waldinger R.J.: Toward automatic program synthesis. Commun. ACM 14(3), 151\u2013165 (1971)","journal-title":"Commun. ACM"},{"issue":"1","key":"223_CR44","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z. Manna","year":"1980","unstructured":"Manna Z., Waldinger R.J.: A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst. 2(1), 90\u2013121 (1980)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"223_CR45","unstructured":"Mayer, M., Suter, P., Piskac, R., Kuncak, V.: Comfusy: complete functional synthesis (tool presentation). In: CAV (2010)"},{"key":"223_CR46","doi-asserted-by":"crossref","unstructured":"McCarthy, J., Painter, J.: Correctness of a compiler for arithmetic expressions. In: Proceedings of Symposia in Applied Mathematics. American Mathematical Society, pp. 33\u201341. (1967)","DOI":"10.1090\/psapm\/019\/0242403"},{"key":"223_CR47","unstructured":"McDonald, J., Anton, J.: SPECWARE\u2014producing software correct by construction. Technical report KES.U.01.3. (2001)"},{"key":"223_CR48","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1145\/319301.319350","volume":"21","author":"J.M. Morris","year":"1999","unstructured":"Morris J.M., Bunkenburg A.: Specificational functions. ACM Trans. Program. Lang. Syst. 21, 677\u2013701 (1999)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"223_CR49","doi-asserted-by":"crossref","unstructured":"Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid types. In: PLDI, pp. 159\u2013169. (2008)","DOI":"10.1145\/1379022.1375602"},{"key":"223_CR50","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constraint-based linear-relations analysis. In: SAS, pp. 53\u201368. (2004)","DOI":"10.1007\/978-3-540-27864-1_7"},{"key":"223_CR51","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: VMCAI, pp. 25\u201341. (2005)","DOI":"10.1007\/978-3-540-30579-8_2"},{"key":"223_CR52","volume-title":"Theory of Linear and Integer Programming","author":"A. Schrijver","year":"1986","unstructured":"Schrijver A.: Theory of Linear and Integer Programming. Wiley, New York, NY (1986)"},{"issue":"9","key":"223_CR53","doi-asserted-by":"crossref","first-page":"1024","DOI":"10.1109\/32.58788","volume":"16","author":"D.R. Smith","year":"1990","unstructured":"Smith D.R.: Kids: a semiautomatic program development system. IEEE Trans. Softw. Eng. 16(9), 1024\u20131043 (1990)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"223_CR54","doi-asserted-by":"crossref","unstructured":"Smith, D.R.: Designware: Software Development by Refinement, Invited talk CTCS\u201999, Edinburgh, Scotland, pp. 3\u201321. (2001)","DOI":"10.1007\/978-1-4615-1391-9_1"},{"key":"223_CR55","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Arnold, G., Tancau, L., Bodik, R., Saraswat, V., Seshia, S.: Sketching stencils. In: PLDI, pp. 167\u2013178. (2007)","DOI":"10.1145\/1273442.1250754"},{"key":"223_CR56","unstructured":"Srivastava, S.: Satisfiability-based program reasoning and program synthesis. PhD thesis, University of Maryland, College Park. http:\/\/www.cs.umd.edu\/~saurabhs\/pubs\/saurabh-srivastava-thesis-9pt.pdf (2010)"},{"key":"223_CR57","doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S.: Program verification using templates over predicate abstraction. In: PLDI (2009)","DOI":"10.1145\/1542476.1542501"},{"key":"223_CR58","doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: VS3: SMT solvers for program verification. In: CAV (2009)","DOI":"10.1007\/978-3-642-02658-4_58"},{"key":"223_CR59","doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: POPL (2010)","DOI":"10.1145\/1706299.1706337"},{"key":"223_CR60","doi-asserted-by":"crossref","unstructured":"Thies, W., Karczmarek, M., Amarasinghe, S.P.: Streamit: a language for streaming applications. In: CC, pages 179\u2013196. (2002)","DOI":"10.1007\/3-540-45937-5_14"},{"key":"223_CR61","doi-asserted-by":"crossref","unstructured":"Vechev, M., Yahav, E., Yorsh, G.: Abstraction-guided synthesis of synchronization. In: POPL, pp. 327\u2013338. (2010)","DOI":"10.1145\/1707801.1706338"},{"key":"223_CR62","unstructured":"Waldinger, R.J., Lee, R.C.T.: Prow: a step toward automatic program writing. In: IJCAI, pp. 241\u2013252. (1969)"},{"key":"223_CR63","doi-asserted-by":"crossref","unstructured":"Wang, C., Yang, Z., Gupta, A., Ivancic, F.: Using counterexamples for improving the precision of reachability computation with polyhedra. In: CAV, pp. 352\u2013365. (2007)","DOI":"10.1007\/978-3-540-73368-3_40"},{"key":"223_CR64","doi-asserted-by":"crossref","unstructured":"Xie, Y., Aiken, A.: Saturn: a sat-based tool for bug detection. In: CAV, pp. 139\u2013143. (2005)","DOI":"10.1007\/11513988_13"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0223-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-012-0223-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0223-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T06:30:30Z","timestamp":1742365830000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-012-0223-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1,25]]},"references-count":64,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2013,10]]}},"alternative-id":["223"],"URL":"https:\/\/doi.org\/10.1007\/s10009-012-0223-4","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,1,25]]}}}