{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T11:32:39Z","timestamp":1768908759816,"version":"3.49.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031331695","type":"print"},{"value":"9783031331701","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-33170-1_23","type":"book-chapter","created":{"date-parts":[[2023,6,2]],"date-time":"2023-06-02T12:55:27Z","timestamp":1685710527000},"page":"380-396","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Condition Synthesis Realizability via\u00a0Constrained Horn Clauses"],"prefix":"10.1007","author":[{"given":"Bat-Chen","family":"Rothenberg","sequence":"first","affiliation":[]},{"given":"Orna","family":"Grumberg","sequence":"additional","affiliation":[]},{"given":"Yakir","family":"Vizel","sequence":"additional","affiliation":[]},{"given":"Eytan","family":"Singher","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,6,3]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, 20\u201323 October 2013, pp. 1\u20138. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-642-28756-5_38","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2012","unstructured":"Beyer, D.: Competition on software verification. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 504\u2013524. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_38"},{"key":"23_CR3","unstructured":"Bhatia, S., Padhi, S., Natarajan, N., Sharma, R., Jain, P.: OASIS: ILP-guided synthesis of loop invariants. CoRR (2019)"},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-319-23534-9_2","volume-title":"Fields of Logic and Computation II","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24\u201351. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23534-9_2"},{"key":"23_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-39611-3_24","volume-title":"Hardware and Software: Verification and Testing","author":"R Bloem","year":"2013","unstructured":"Bloem, R., et al.: FoREnSiC\u2013 an automatic debugging environment for C programs. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 260\u2013265. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39611-3_24"},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"DeMarco, F., Xuan, J., Le Berre, D., Monperrus, M.: Automatic repair of buggy if conditions and missing preconditions with SMT. In: Proceedings of the 6th International Workshop on Constraints in Software Testing, Verification, and Analysis, pp. 30\u201339. ACM (2014)","DOI":"10.1145\/2593735.2593740"},{"issue":"4","key":"23_CR7","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/s10664-005-3861-2","volume":"10","author":"H Do","year":"2005","unstructured":"Do, H., Elbaum, S., Rothermel, G.: Supporting controlled experimentation with testing techniques: an infrastructure and its potential impact. Empir. Softw. Eng. 10(4), 405\u2013435 (2005)","journal-title":"Empir. Softw. Eng."},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"Farzan, A., Lette, D., Nicolet, V.: Recursion synthesis with unrealizability witnesses. In: Jhala, R., Dillig, I. (eds.) PLDI 2022: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, 13\u201317 June 2022, pp. 244\u2013259. ACM (2022)","DOI":"10.1145\/3519939.3523726"},{"key":"23_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-030-30048-7_32","volume-title":"Principles and Practice of Constraint Programming","author":"G Fedyukovich","year":"2019","unstructured":"Fedyukovich, G., Gupta, A.: Functional synthesis with examples. In: Schiex, T., de Givry, S. (eds.) CP 2019. LNCS, vol. 11802, pp. 547\u2013564. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30048-7_32"},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20"},{"key":"23_CR11","doi-asserted-by":"publisher","unstructured":"Hu, Q., Breck, J., Cyphert, J., D\u2019Antoni, L., Reps, T.W.: Proving unrealizability for syntaxguided synthesis. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV 2019. LNCS, vol. 11561, pp. 335\u2013352. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_18","DOI":"10.1007\/978-3-030-25540-4_18"},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"Hu, Q., D\u2019Antoni, L., Cyphert, J., Reps, T.: Exact and approximate unrealizability of syntax-guided synthesis problems. In: PLDI (2020)","DOI":"10.1145\/3395631"},{"key":"23_CR13","unstructured":"Hu, Q., Evavold, I., Samanta, R., Singh, R., D\u2019Antoni, L.: Program repair via direct state manipulation (2018)"},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"Huang, K., Qiu, X., Shen, P., Wang, Y.: Reconciling enumerative and deductive program synthesis. In: PLDI, pp. 1159\u20131174 (2020)","DOI":"10.1145\/3385412.3386027"},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"Kim, J., D\u2019Antoni, L., Reps, T.W.: Unrealizability logic. In: POPL 2023: Proceedings of the 50th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM (2023)","DOI":"10.1145\/3571216"},{"key":"23_CR16","doi-asserted-by":"crossref","unstructured":"Kim, J., Hu, Q., D\u2019Antoni, L., Reps, T.W.: Semantics guided synthesis. In: POPL (2020)","DOI":"10.1145\/3434311"},{"issue":"3","key":"23_CR17","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-016-0249-4","volume":"48","author":"A Komuravelli","year":"2016","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Formal Methods Syst. Des. 48(3), 175\u2013205 (2016)","journal-title":"Formal Methods Syst. Des."},{"key":"23_CR18","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":"23_CR19","doi-asserted-by":"crossref","unstructured":"Long, F., Rinard, M.: Staged program repair with condition synthesis. In: ESEC\/FSE, pp. 166\u2013178. ACM (2015)","DOI":"10.1145\/2786805.2786811"},{"key":"23_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-030-11245-5_4","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T-T Nguyen","year":"2019","unstructured":"Nguyen, T.-T., Ta, Q.-T., Chin, W.-N.: Automatic program repair using formal verification and expression templates. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 70\u201391. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-11245-5_4"},{"key":"23_CR21","unstructured":"Padhi, S., Sharma, R., Millstein, T.: LoopInvGen: a loop invariant generator based on precondition inference. arXiv (2017)"},{"key":"23_CR22","doi-asserted-by":"crossref","unstructured":"Polozov, O., Gulwani, S.: FlashMeta: a framework for inductive program synthesis. In: OOPSLA, vol. 25\u201330-Oct-, pp. 107\u2013126 (2015)","DOI":"10.1145\/2858965.2814310"},{"key":"23_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-030-25543-5_5","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2019","unstructured":"Reynolds, A., Barbosa, H., N\u00f6tzli, A., Barrett, C., Tinelli, C.: cvc4sy: smart and fast term enumeration for syntax-guided synthesis. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 74\u201383. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_5"},{"key":"23_CR24","doi-asserted-by":"crossref","unstructured":"Si, X., Lee, W., Zhang, R., Albarghouthi, A., Koutris, P., Naik, M.: Syntax-guided synthesis of datalog programs. In: ESEC\/FSE, pp. 515\u2013527 (2018)","DOI":"10.1145\/3236024.3236034"},{"key":"23_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-319-66706-5_18","volume-title":"Static Analysis","author":"S So","year":"2017","unstructured":"So, S., Oh, H.: Synthesizing imperative programs from examples guided by static analysis. In: Ranzato, F. (ed.) SAS 2017. LNCS, vol. 10422, pp. 364\u2013381. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66706-5_18"},{"key":"23_CR26","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bodik, R., Saraswat, V., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. In: ACM Sigplan Notices, vol. 41, pp. 404\u2013415. ACM (2006)","DOI":"10.1145\/1168918.1168907"},{"key":"23_CR27","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":"23_CR28","doi-asserted-by":"crossref","unstructured":"Wang, X., Dillig, I., Singh, R.: Program synthesis using abstraction refinement. arXiv, 2(January 2018) (2017)","DOI":"10.1145\/3158151"},{"key":"23_CR29","doi-asserted-by":"crossref","unstructured":"Xiong, Y., et al.: Precise condition synthesis for program repair. In: ICSE (2017)","DOI":"10.1109\/ICSE.2017.45"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-33170-1_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,2]],"date-time":"2023-06-02T12:59:38Z","timestamp":1685710778000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-33170-1_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031331695","9783031331701"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-33170-1_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"3 June 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Houston, TX","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 May 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/nfm-2023","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"75","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"35% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.9","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}