{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,3]],"date-time":"2025-07-03T04:05:52Z","timestamp":1751515552491,"version":"3.41.0"},"publisher-location":"Singapore","reference-count":20,"publisher":"Springer Nature Singapore","isbn-type":[{"type":"print","value":"9789819646555"},{"type":"electronic","value":"9789819646562"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"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":[[2025]]},"DOI":"10.1007\/978-981-96-4656-2_7","type":"book-chapter","created":{"date-parts":[[2025,4,5]],"date-time":"2025-04-05T13:18:26Z","timestamp":1743859106000},"page":"155-170","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Automating Component-Based Embedded Software Construction via\u00a0Formal Synthesis and\u00a0LLMs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-4708-914X","authenticated-orcid":false,"given":"Sirui","family":"Liu","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8033-7943","authenticated-orcid":false,"given":"Wei","family":"Dong","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0004-7508-0348","authenticated-orcid":false,"given":"Tiecheng","family":"Ma","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0005-2900-5467","authenticated-orcid":false,"given":"Yanqi","family":"Dong","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0003-8436-0010","authenticated-orcid":false,"given":"Dong","family":"Yang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,4,5]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","unstructured":"Achiam, J., et\u00a0al.: GPT-4 technical report. arXiv (2023). https:\/\/doi.org\/10.48550\/2303.08774","DOI":"10.48550\/2303.08774"},{"key":"7_CR2","unstructured":"Bai, J., et al.: Qwen technical report. arXiv (2023). https:\/\/doi.org\/10.48550\/2309.16609 (2023)"},{"key":"7_CR3","doi-asserted-by":"publisher","unstructured":"Bi, X., et\u00a0al.: Deepseek LLM: scaling open-source language models with longtermism. arXiv (2024). https:\/\/doi.org\/10.48550\/2401.02954","DOI":"10.48550\/2401.02954"},{"issue":"3","key":"7_CR4","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","volume":"78","author":"R Bloem","year":"2012","unstructured":"Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. J. Comput. Syst. Sci. 78(3), 911\u2013938 (2012). https:\/\/doi.org\/10.1016\/j.jcss.2011.08.007","journal-title":"J. Comput. Syst. Sci."},{"key":"7_CR5","unstructured":"Bocchino, R., Canham, T., Watney, G., Reder, L., Levison, J.: F prime: an open-source framework for small-scale flight software systems. In: Proceedings of the 32nd Annual AIAA\/USU Conference on Small Satellites (2018). https:\/\/digitalcommons.usu.edu\/smallsat\/2018\/all2018\/328\/"},{"key":"7_CR6","doi-asserted-by":"publisher","unstructured":"Brown, T., et\u00a0al.: Language models are few-shot learners. In: NIPS\u201920: Proceedings of the 34th International Conference on Neural Information Processing Systems, pp. 1877\u20131901 (2020). https:\/\/doi.org\/10.5555\/3495724.3495883","DOI":"10.5555\/3495724.3495883"},{"key":"7_CR7","doi-asserted-by":"publisher","unstructured":"Chen, Y., Gandhi, R., Zhang, Y., Fan, C.: NL2TL: transforming natural languages to temporal logics using large language models. arXiv (2023). https:\/\/doi.org\/10.48550\/2305.07766","DOI":"10.48550\/2305.07766"},{"key":"7_CR8","doi-asserted-by":"publisher","unstructured":"Cosler, M., Hahn, C., Mendoza, D., Schmitt, F., Trippel, C.: NL2SPEC: interactively translating unstructured natural language to temporal logics with large language models. In: Enea, C., Lal, A. (eds.) CAV 2023. LNCS, vol. 13965, pp. 383\u2013396 (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_18","DOI":"10.1007\/978-3-031-37703-7_18"},{"key":"7_CR9","doi-asserted-by":"publisher","unstructured":"Diao, S., Wang, P., Lin, Y., Pan, R., Liu, X., Zhang, T.: Active prompting with chain-of-thought for large language models. arXiv (2023).https:\/\/doi.org\/10.48550\/2302.12246","DOI":"10.48550\/2302.12246"},{"key":"7_CR10","doi-asserted-by":"publisher","unstructured":"Finucane, C., Jing, G., Kress-Gazit, H.: LTLMoP: experimenting with language, temporal logic and robot control. In: 2010 IEEE\/RSJ International Conference on Intelligent Robots and Systems, pp. 1988\u20131993. IEEE (2010). https:\/\/doi.org\/10.1109\/IROS.2010.5650371","DOI":"10.1109\/IROS.2010.5650371"},{"key":"7_CR11","doi-asserted-by":"publisher","unstructured":"Fuggitti, F., Chakraborti, T.: NL2LTL \u2013 a Python package for converting natural language (NL) instructions to linear temporal logic (LTL) formulas. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a037, pp. 16428\u201316430 (2023). https:\/\/doi.org\/10.1609\/aaai.v37i13.27068","DOI":"10.1609\/aaai.v37i13.27068"},{"key":"7_CR12","doi-asserted-by":"publisher","unstructured":"Jing, G., Finucane, C., Raman, V., Kress-Gazit, H.: Correct high-level robot control from structured English. In: 2012 IEEE International Conference on Robotics and Automation, pp. 3543\u20133544 (2012). https:\/\/doi.org\/10.1109\/ICRA.2012.6225161","DOI":"10.1109\/ICRA.2012.6225161"},{"key":"7_CR13","doi-asserted-by":"publisher","unstructured":"Lialin, V., Deshpande, V., Rumshisky, A.: Scaling down to scale up: a guide to parameter-efficient fine-tuning. arXiv (2023). https:\/\/doi.org\/10.48550\/2303.15647","DOI":"10.48550\/2303.15647"},{"key":"7_CR14","doi-asserted-by":"publisher","unstructured":"Mikolov, T.: Efficient estimation of word representations in vector space. arXiv (2013). https:\/\/doi.org\/10.48550\/1301.3781","DOI":"10.48550\/1301.3781"},{"key":"7_CR15","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), pp. 46\u201357. IEEE (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"7_CR16","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Ausiello, G., Dezani-Ciancaglini, M., Della Rocca, S.R. (eds.) Automata, Languages and Programming, 16th International Colloquium. LNCS, vol.\u00a0372, pp. 652\u2013671. Springer, Cham (1989). https:\/\/doi.org\/10.1007\/BFb0035790","DOI":"10.1007\/BFb0035790"},{"key":"7_CR17","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Sa\u2019ar, Y., Zuck, L.D.: JTLV: a framework for developing verification algorithms. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 171\u2013174. Springer, Cham (2010). https:\/\/doi.org\/10.1007\/BFb0035790","DOI":"10.1007\/BFb0035790"},{"key":"7_CR18","doi-asserted-by":"publisher","unstructured":"Reimers, N.: Sentence-BERT: sentence embeddings using Siamese BERT-networks. arXiv (2019). https:\/\/doi.org\/10.48550\/arXiv.1908.10084","DOI":"10.48550\/arXiv.1908.10084"},{"issue":"3","key":"7_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/361768","volume":"56","author":"H Zhang","year":"2023","unstructured":"Zhang, H., Song, H., Li, S., Zhou, M., Song, D.: A survey of controllable text generation using transformer-based pre-trained language models. ACM Comput. Surv. 56(3), 1\u201337 (2023). https:\/\/doi.org\/10.1145\/361768","journal-title":"ACM Comput. Surv."},{"key":"7_CR20","doi-asserted-by":"publisher","unstructured":"Zhao, Z., et\u00a0al.: Recommender systems in the era of large language models (LLMs). arXiv (2023). https:\/\/doi.org\/10.48550\/2307.02046","DOI":"10.48550\/2307.02046"}],"container-title":["Lecture Notes in Computer Science","Engineering Trustworthy Software Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-96-4656-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,2]],"date-time":"2025-07-02T11:01:42Z","timestamp":1751454102000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-96-4656-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9789819646555","9789819646562"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-981-96-4656-2_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"5 April 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}