{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,4]],"date-time":"2026-10-04T11:54:54Z","timestamp":1791114894952,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":38,"publisher":"ACM","license":[{"start":{"date-parts":[[2010,1,17]],"date-time":"2010-01-17T00:00:00Z","timestamp":1263686400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2010,1,17]]},"DOI":"10.1145\/1706299.1706337","type":"proceedings-article","created":{"date-parts":[[2010,1,19]],"date-time":"2010-01-19T15:15:04Z","timestamp":1263914104000},"page":"313-326","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":163,"title":["From program verification to program synthesis"],"prefix":"10.1145","author":[{"given":"Saurabh","family":"Srivastava","sequence":"first","affiliation":[{"name":"University of Maryland, College Park, College Park, MD, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sumit","family":"Gulwani","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, WA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jeffrey S.","family":"Foster","sequence":"additional","affiliation":[{"name":"University of Maryland, College Park, College Park, MD, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2010,1,17]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"D. Basin Y. DeVille P. Flener A. Hamfelt and J.F. NIlsson. Synthesis of programs in computational logic. In LNCS 3049.  D. Basin Y. DeVille P. Flener A. Hamfelt and J.F. NIlsson. Synthesis of programs in computational logic. In LNCS 3049."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/993954"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/648063.747438"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734089"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11506676_11"},{"key":"e_1_3_2_1_6_1","volume-title":"CAV'03","author":"Colon Michael","unstructured":"Michael Colon , Sriram Sankaranarayanan , and Henny Sipma . Linear invariant generation using non-linear constraint solving . In CAV'03 . Michael Colon, Sriram Sankaranarayanan, and Henny Sipma. Linear invariant generation using non-linear constraint solving. In CAV'03."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"e_1_3_2_1_8_1","unstructured":"T. Cormen C. Leiserson and R. Rivest. Introduction to Algorithms.   T. Cormen C. Leiserson and R. Rivest. Introduction to Algorithms."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_10_1","unstructured":"Leonardo de Moura and Nikolaj Bjorner. Z3 2008. http:\/\/research.microsoft.com\/projects\/Z3\/.  Leonardo de Moura and Nikolaj Bjorner. Z3 2008. http:\/\/research.microsoft.com\/projects\/Z3\/."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01933419"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate Calculus and Program Semantics. Texts and Monographs in CS","author":"Dijkstra Edsger W.","year":"1990","unstructured":"Edsger W. Dijkstra and Carel S. Scholten . Predicate Calculus and Program Semantics. Texts and Monographs in CS . 1990 . Edsger W. Dijkstra and Carel S. Scholten. Predicate Calculus and Program Semantics. Texts and Monographs in CS. 1990."},{"key":"e_1_3_2_1_14_1","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger Wybe","year":"1976","unstructured":"Edsger Wybe Dijkstra . A Discipline of Programming . 1976 . Edsger Wybe Dijkstra. A Discipline of Programming. 1976."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/800178.810159"},{"key":"e_1_3_2_1_16_1","volume-title":"SMT'08","author":"Filliatre Jean-Christophe","unstructured":"Jean-Christophe Filliatre . Using SMT solvers for deductive verification of C and Java programs . In SMT'08 . Jean-Christophe Filliatre. Using SMT solvers for deductive verification of C and Java programs. In SMT'08."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1999.0348"},{"key":"e_1_3_2_1_18_1","volume-title":"The Science of Programming","author":"Gries David","year":"1987","unstructured":"David Gries . The Science of Programming . 1987 . David Gries. The Science of Programming. 1987."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_33"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-93900-9_13"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375616"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/800152.804919"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2006.22"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_23"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328461"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/362566.362568"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250754"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375599"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065045"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542501"},{"key":"e_1_3_2_1_33_1","unstructured":"Saurabh Srivastava Sumit Gulwani and Jeffrey S. Foster. VS3 . http:\/\/www.cs.umd.edu\/~saurabhs\/pacs\/.  Saurabh Srivastava Sumit Gulwani and Jeffrey S. Foster. VS3 . http:\/\/www.cs.umd.edu\/~saurabhs\/pacs\/."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_58"},{"key":"e_1_3_2_1_35_1","volume-title":"Microsoft Research","author":"Srivastava Saurabh","year":"2009","unstructured":"Saurabh Srivastava , Sumit Gulwani , and Jeffrey S. Foster . Proof-theoretic program synthesis: From program verification to program synthesis. Technical report , Microsoft Research , Redmond , 2009 . Saurabh Srivastava, Sumit Gulwani, and Jeffrey S. Foster. Proof-theoretic program synthesis: From program verification to program synthesis. Technical report, Microsoft Research, Redmond, 2009."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_13"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706338"},{"key":"e_1_3_2_1_38_1","volume-title":"Systematic Programming: An Introduction","author":"Wirth Nicholas","year":"1973","unstructured":"Nicholas Wirth . Systematic Programming: An Introduction . 1973 . Nicholas Wirth. Systematic Programming: An Introduction. 1973."}],"event":{"name":"POPL '10: The 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Madrid Spain","acronym":"POPL '10","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1706299.1706337","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1706299.1706337","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:26:19Z","timestamp":1750263979000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1706299.1706337"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,1,17]]},"references-count":38,"alternative-id":["10.1145\/1706299.1706337","10.1145\/1706299"],"URL":"https:\/\/doi.org\/10.1145\/1706299.1706337","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1707801.1706337","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2010,1,17]]},"assertion":[{"value":"2010-01-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}