{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T03:58:27Z","timestamp":1782878307128,"version":"3.54.5"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031453281","type":"print"},{"value":"9783031453298","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-45329-8_12","type":"book-chapter","created":{"date-parts":[[2023,10,21]],"date-time":"2023-10-21T18:02:40Z","timestamp":1697911360000},"page":"248-269","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Reactive Synthesis of\u00a0Smart Contract Control Flows"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4280-8441","authenticated-orcid":false,"given":"Bernd","family":"Finkbeiner","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1660-2949","authenticated-orcid":false,"given":"Jana","family":"Hofmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9672-2398","authenticated-orcid":false,"given":"Florian","family":"Kohn","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7781-043X","authenticated-orcid":false,"given":"Noemi","family":"Passing","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,10,22]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","unstructured":"Antonino, P., Ferreira, J., Sampaio, A., Roscoe, A.W.: Specification is law: safe creation and upgrade of ethereum smart contracts. CoRR abs\/2205.07529 (2022). https:\/\/doi.org\/10.48550\/arXiv.2205.07529","DOI":"10.48550\/arXiv.2205.07529"},{"key":"12_CR2","unstructured":"Avolabs: NFT auction reference contract. https:\/\/github.com\/avolabs-io\/nft-auction (2022). Accessed 05 July 2022"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Choi, W., Finkbeiner, B., Piskac, R., Santolucito, M.: Can reactive synthesis and syntax-guided synthesis be friends? In: 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (2022). https:\/\/publications.cispa.saarland\/3674\/","DOI":"10.1145\/3519939.3523429"},{"key":"12_CR4","doi-asserted-by":"publisher","unstructured":"Ciccio, C.D., et al.: Blockchain support for collaborative business processes. Inform. Spektrum 42(3), 182\u2013190 (2019). https:\/\/doi.org\/10.1007\/s00287-019-01178-x","DOI":"10.1007\/s00287-019-01178-x"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-30494-4_18","volume-title":"Formal Methods in Computer-Aided Design","author":"A Cimatti","year":"2004","unstructured":"Cimatti, A., Roveri, M., Sheridan, D.: Bounded verification of past LTL. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 245\u2013259. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30494-4_18"},{"key":"12_CR6","unstructured":"Dharanikota, S., Mukherjee, S., Bhardwaj, C., Rastogi, A., Lal, A.: Celestial: a smart contracts verification framework. In: Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design (FMCAD 2021), pp. 133\u2013142 (2021)"},{"key":"12_CR7","unstructured":"Ethereum: Introduction to ethereum (2021). https:\/\/ethereum.org\/en\/developers\/docs\/intro-to-ethereum\/ . Accessed 05 July 2022"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-030-99253-8_17","volume-title":"Foundations of Software Science and Computation Structures","author":"B Finkbeiner","year":"2022","unstructured":"Finkbeiner, B., Heim, P., Passing, N.: Temporal stream logic modulo theories. In: FoSSaCS 2022. LNCS, vol. 13242, pp. 325\u2013346. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99253-8_17"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Hofmann, J., Kohn, F., Passing, N.: Reactive synthesis of smart contract control flows (2023)","DOI":"10.1007\/978-3-031-45329-8_12"},{"key":"12_CR10","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Klein, F., Piskac, R., Santolucito, M.: Synthesizing functional reactive programs. In: Eisenberg, R.A. (ed.) Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell, Haskell@ICFP 2019, Berlin, Germany, 18\u201323 August 2019, pp. 162\u2013175. ACM (2019). https:\/\/doi.org\/10.1145\/3331545.3342601","DOI":"10.1145\/3331545.3342601"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"609","DOI":"10.1007\/978-3-030-25540-4_35","volume-title":"Computer Aided Verification","author":"B Finkbeiner","year":"2019","unstructured":"Finkbeiner, B., Klein, F., Piskac, R., Santolucito, M.: Temporal stream logic: synthesis beyond the bools. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 609\u2013629. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_35"},{"key":"12_CR12","unstructured":"Geier, G., Heim, P., Klein, F., Finkbeiner, B.: Syntroids: synthesizing a game for FPGAS using temporal logic specifications. CoRR abs\/2101.07232 (2021). https:\/\/arxiv.org\/abs\/2101.07232"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-46002-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Havelund","year":"2002","unstructured":"Havelund, K., Ro\u015fu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342\u2013356. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46002-0_24"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Hopcroft, J.: An n log n algorithm for minimizing states in a finite automaton. In: Theory of Machines and Computations, pp. 189\u2013196. Elsevier (1971)","DOI":"10.1016\/B978-0-12-417750-5.50022-1"},{"key":"12_CR15","doi-asserted-by":"publisher","unstructured":"Jacobs, S., Bloem, R.: Parameterized synthesis. Log. Methods Comput. Sci. 10(1) (2014). https:\/\/doi.org\/10.2168\/LMCS-10(1:12)2014","DOI":"10.2168\/LMCS-10(1:12)2014"},{"key":"12_CR16","doi-asserted-by":"publisher","unstructured":"Kalra, S., Goel, S., Dhawan, M., Sharma, S.: ZEUS: analyzing safety of smart contracts. In: 25th Annual Network and Distributed System Security Symposium, NDSS 2018, San Diego, California, USA, 18-21 February 2018. The Internet Society (2018). https:\/\/doi.org\/10.14722\/ndss.2018.23082","DOI":"10.14722\/ndss.2018.23082"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"928","DOI":"10.1007\/978-3-642-39799-8_66","volume-title":"Computer Aided Verification","author":"A Khalimov","year":"2013","unstructured":"Khalimov, A., Jacobs, S., Bloem, R.: PARTY parameterized synthesis of token rings. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 928\u2013933. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_66"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-642-35873-9_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Khalimov","year":"2013","unstructured":"Khalimov, A., Jacobs, S., Bloem, R.: Towards efficient parameterized synthesis. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 108\u2013127. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_9"},{"key":"12_CR19","unstructured":"Klein, F., Santolucito, M.: TSL tools (2019). https:\/\/github.com\/kleinreact\/tsltools"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/3-540-48683-6_17","volume-title":"Computer Aided Verification","author":"O Kupferman","year":"1999","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 172\u2013183. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_17"},{"key":"12_CR21","unstructured":"Lahiri, S.K., Chen, S., Wang, Y., Dillig, I.: Formal specification and verification of smart contracts for azure blockchain. CoRR abs\/1812.08829 (2018). https:\/\/arxiv.org\/abs\/1812.08829"},{"key":"12_CR22","doi-asserted-by":"publisher","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3(2), 125\u2013143 (1977). https:\/\/doi.org\/10.1109\/TSE.1977.229904","DOI":"10.1109\/TSE.1977.229904"},{"key":"12_CR23","doi-asserted-by":"publisher","unstructured":"Lisitsa, A., Potapov, I.: Temporal logic with predicate lambda-abstraction. In: 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), 23\u201325 June 2005, Burlington, Vermont, USA, pp. 147\u2013155. IEEE Computer Society (2005). https:\/\/doi.org\/10.1109\/TIME.2005.34","DOI":"10.1109\/TIME.2005.34"},{"key":"12_CR24","doi-asserted-by":"publisher","unstructured":"L\u00f3pez-Pintado, O., Garc\u00eda-Ba\u00f1uelos, L., Dumas, M., Weber, I., Ponomarev, A.: Caterpillar: a business process execution engine on the ethereum blockchain. Softw. Pract. Exp. 49(7), 1162\u20131193 (2019). https:\/\/doi.org\/10.1002\/spe.2702","DOI":"10.1002\/spe.2702"},{"key":"12_CR25","unstructured":"Maderbacher, B., Bloem, R.: Reactive synthesis modulo theories using abstraction refinement. CoRR abs\/2108.00090 (2021). https:\/\/arxiv.org\/abs\/2108.00090"},{"key":"12_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-030-64437-6_14","volume-title":"Programming Languages and Systems","author":"O Markgraf","year":"2020","unstructured":"Markgraf, O., Hong, C.-D., Lin, A.W., Najib, M., Neider, D.: Parameterized synthesis with safety properties. In: Oliveira, B.C.S. (ed.) APLAS 2020. LNCS, vol. 12470, pp. 273\u2013292. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-64437-6_14"},{"key":"12_CR27","doi-asserted-by":"publisher","unstructured":"Mavridou, A., Laszka, A.: Designing secure ethereum smart contracts: a finite state machine based approach. In: Meiklejohn, S., Sako, K. (eds.) FC 2018. LNCS, vol. 10957, pp. 523\u2013540. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-662-58387-6_28","DOI":"10.1007\/978-3-662-58387-6_28"},{"key":"12_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/978-3-030-32101-7_27","volume-title":"Financial Cryptography and Data Security","author":"A Mavridou","year":"2019","unstructured":"Mavridou, A., Laszka, A., Stachtiari, E., Dubey, A.: VeriSolid: correct-by-design smart contracts for ethereum. In: Goldberg, I., Moore, T. (eds.) FC 2019. LNCS, vol. 11598, pp. 446\u2013465. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32101-7_27"},{"issue":"1\u20133","key":"12_CR29","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/S0304-3975(02)00646-1","volume":"297","author":"R Mayr","year":"2003","unstructured":"Mayr, R.: Undecidable problems in unreliable computations. Theor. Comput. Sci. 297(1\u20133), 337\u2013354 (2003). https:\/\/doi.org\/10.1016\/S0304-3975(02)00646-1","journal-title":"Theor. Comput. Sci."},{"issue":"5","key":"12_CR30","doi-asserted-by":"publisher","first-page":"1045","DOI":"10.1002\/j.1538-7305.1955.tb03788.x","volume":"34","author":"GH Mealy","year":"1955","unstructured":"Mealy, G.H.: A method for synthesizing sequential circuits. Bell Syst. Tech. J. 34(5), 1045\u20131079 (1955). https:\/\/doi.org\/10.1002\/j.1538-7305.1955.tb03788.x","journal-title":"Bell Syst. Tech. J."},{"key":"12_CR31","doi-asserted-by":"crossref","unstructured":"Nehai, Z., Piriou, P.Y., Daumas, F.: Model-checking of smart contracts. In: 2018 IEEE International Conference on Internet of Things (iThings) and IEEE Green Computing and Communications (GreenCom) and IEEE Cyber, Physical and Social Computing (CPSCom) and IEEE Smart Data (SmartData), pp. 980\u2013987. IEEE (2018)","DOI":"10.1109\/Cybermatics_2018.2018.00185"},{"key":"12_CR32","unstructured":"Open Zeppelin: Erc20 token system documentation from open zeppelin (2022). https:\/\/docs.openzeppelin.com\/contracts\/2.x\/api\/token\/erc20. Accessed 05 July 2022"},{"key":"12_CR33","doi-asserted-by":"publisher","unstructured":"Permenev, A., Dimitrov, D.K., Tsankov, P., Drachsler-Cohen, D., Vechev, M.T.: VerX: safety verification of smart contracts. In: 2020 IEEE Symposium on Security and Privacy, SP 2020, San Francisco, CA, USA, 18\u201321 May 2020, pp. 1661\u20131677. IEEE (2020). https:\/\/doi.org\/10.1109\/SP40000.2020.00024","DOI":"10.1109\/SP40000.2020.00024"},{"key":"12_CR34","doi-asserted-by":"publisher","unstructured":"Stephens, J., Ferles, K., Mariano, B., Lahiri, S.K., Dillig, I.: SmartPulse: automated checking of temporal properties in smart contracts. In: 42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24\u201327 May 2021, pp. 555\u2013571. IEEE (2021). https:\/\/doi.org\/10.1109\/SP40001.2021.00085","DOI":"10.1109\/SP40001.2021.00085"},{"key":"12_CR35","unstructured":"Suvorov, D., Ulyantsev, V.: Smart contract design meets state machine synthesis: Case studies. CoRR abs\/1906.02906 (2019). https:\/\/arxiv.org\/abs\/1906.02906"},{"key":"12_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-030-41600-3_7","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"Y Wang","year":"2020","unstructured":"Wang, Y., et al.: Formal verification of workflow policies for smart contracts in azure blockchain. In: Chakraborty, S., Navas, J.A. (eds.) VSTTE 2019. LNCS, vol. 12031, pp. 87\u2013106. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-41600-3_7"},{"key":"12_CR37","series-title":"Blockchain Technologies","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-981-15-1137-0_4","volume-title":"Blockchain Technology for Industry 4.0","author":"N Zupan","year":"2020","unstructured":"Zupan, N., Kasinathan, P., Cuellar, J., Sauer, M.: Secure smart contract generation based on petri nets. In: Rosa Righi, R., Alberti, A.M., Singh, M. (eds.) Blockchain Technology for Industry 4.0. BT, pp. 73\u201398. Springer, Singapore (2020). https:\/\/doi.org\/10.1007\/978-981-15-1137-0_4"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-45329-8_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,24]],"date-time":"2023-12-24T15:05:19Z","timestamp":1703430319000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-45329-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031453281","9783031453298"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-45329-8_12","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":"22 October 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Singapore","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Singapore","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":"24 October 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 October 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/atva-conference.org\/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":"115","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":"30","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":"0","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":"26% - 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.05","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":"9","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)"}},{"value":"7 tool papers","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}