{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:43:49Z","timestamp":1780994629689,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":49,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,6,18]],"date-time":"2021-06-18T00:00:00Z","timestamp":1623974400000},"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":[[2021,6,19]]},"DOI":"10.1145\/3453483.3454104","type":"proceedings-article","created":{"date-parts":[[2021,6,18]],"date-time":"2021-06-18T13:51:32Z","timestamp":1624024292000},"page":"1203-1217","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["Specification synthesis with constrained Horn clauses"],"prefix":"10.1145","author":[{"given":"Sumanth","family":"Prabhu","sequence":"first","affiliation":[{"name":"TCS Research, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Grigory","family":"Fedyukovich","sequence":"additional","affiliation":[{"name":"Florida State University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kumar","family":"Madhukar","sequence":"additional","affiliation":[{"name":"TCS Research, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Deepak","family":"D'Souza","sequence":"additional","affiliation":[{"name":"IISc Bangalore, India"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,6,18]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837628"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-61499-495-4-1"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040314"},{"key":"e_1_3_2_1_4_1","unstructured":"Rajeev Alur Dana Fisman Saswat Padhi Andrew Reynolds Rishabh Singh and Abhishek Udupa. 2019. SyGuS-Comp 2019. https:\/\/sygus.org\/comp\/2019\/results-slides.pdf  Rajeev Alur Dana Fisman Saswat Padhi Andrew Reynolds Rishabh Singh and Abhishek Udupa. 2019. SyGuS-Comp 2019. https:\/\/sygus.org\/comp\/2019\/results-slides.pdf"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503275"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17502-3_1"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676977"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993524"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535860"},{"key":"e_1_3_2_1_10_1","volume-title":"LPAR (short papers) (EPiC Series in Computing","author":"Bj\u00f8rner Nikolaj","unstructured":"Nikolaj Bj\u00f8rner and Mikol\u00e1s Janota . 2015. Playing with Quantified Satisfaction . In LPAR (short papers) (EPiC Series in Computing , Vol. 35). EasyChair, 15\u2013 27 . https:\/\/easychair.org\/publications\/paper\/jmM Nikolaj Bj\u00f8rner and Mikol\u00e1s Janota. 2015. Playing with Quantified Satisfaction. In LPAR (short papers) (EPiC Series in Computing, Vol. 35). EasyChair, 15\u201327. https:\/\/easychair.org\/publications\/paper\/jmM"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049697.2049700"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_20"},{"key":"e_1_3_2_1_13_1","volume-title":"Parameter synthesis with IC3","author":"Cimatti Alessandro","unstructured":"Alessandro Cimatti , Alberto Griggio , Sergio Mover , and Stefano Tonetta . 2013. Parameter synthesis with IC3 . In FMCAD. IEEE , 165\u2013168. http:\/\/ieeexplore.ieee.org\/document\/6679406\/ Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta. 2013. Parameter synthesis with IC3. In FMCAD. IEEE, 165\u2013168. http:\/\/ieeexplore.ieee.org\/document\/6679406\/"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_10"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_19"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509511"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276501"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062382"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102247"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8603011"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_14"},{"key":"e_1_3_2_1_23_1","unstructured":"Grigory Fedyukovich Philipp R\u00fcmmer and Arie Gurfinkel. 2019. CHC-COMP. https:\/\/chc-comp.github.io\/2019\/chc-comp19.pdf  Grigory Fedyukovich Philipp R\u00fcmmer and Arie Gurfinkel. 2019. CHC-COMP. https:\/\/chc-comp.github.io\/2019\/chc-comp19.pdf"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45251-6_29"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.219.2"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158136"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48288-9_12"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081713"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32759-9_21"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.219.4"},{"key":"e_1_3_2_1_33_1","volume-title":"LPAR (EPiC Series in Computing","volume":"384","author":"Kahsai Temesghen","year":"2017","unstructured":"Temesghen Kahsai , Rody Kersten , Philipp R\u00fcmmer , and Martin Sch\u00e4f . 2017 . Quantified Heap Invariants for Object-Oriented Programs . In LPAR (EPiC Series in Computing , Vol. 46). EasyChair, 368\u2013 384 . https:\/\/easychair.org\/publications\/paper\/Pmh Temesghen Kahsai, Rody Kersten, Philipp R\u00fcmmer, and Martin Sch\u00e4f. 2017. Quantified Heap Invariants for Object-Oriented Programs. In LPAR (EPiC Series in Computing, Vol. 46). EasyChair, 368\u2013384. https:\/\/easychair.org\/publications\/paper\/Pmh"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_19"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993525"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_24"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_18"},{"key":"e_1_3_2_1_39_1","volume-title":"Verifying Safety of Functional Programs with Rosette\/Unbound. CoRR, abs\/1704.04558","author":"Mordvinov Dmitry","year":"2017","unstructured":"Dmitry Mordvinov and Grigory Fedyukovich . 2017. Verifying Safety of Functional Programs with Rosette\/Unbound. CoRR, abs\/1704.04558 ( 2017 ), https:\/\/github.com\/dvvrd\/rosette Dmitry Mordvinov and Grigory Fedyukovich. 2017. Verifying Safety of Functional Programs with Rosette\/Unbound. CoRR, abs\/1704.04558 (2017), https:\/\/github.com\/dvvrd\/rosette"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908099"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99725-4_20"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250749"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_5"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390666"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_25"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273463.1273487"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1134285.1134325"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03542-0_21"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192416"}],"event":{"name":"PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"Virtual Canada","acronym":"PLDI '21","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3453483.3454104","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3453483.3454104","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:48Z","timestamp":1750193268000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3453483.3454104"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,18]]},"references-count":49,"alternative-id":["10.1145\/3453483.3454104","10.1145\/3453483"],"URL":"https:\/\/doi.org\/10.1145\/3453483.3454104","relation":{},"subject":[],"published":{"date-parts":[[2021,6,18]]},"assertion":[{"value":"2021-06-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}