{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T10:15:16Z","timestamp":1770977716041,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":45,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,4,14]],"date-time":"2024-04-14T00:00:00Z","timestamp":1713052800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001871","name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","doi-asserted-by":"publisher","award":["UIDB\/50021\/2020"],"award-info":[{"award-number":["UIDB\/50021\/2020"]}],"id":[{"id":"10.13039\/501100001871","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001871","name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","doi-asserted-by":"publisher","award":["LA\/P\/0063\/2020"],"award-info":[{"award-number":["LA\/P\/0063\/2020"]}],"id":[{"id":"10.13039\/501100001871","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,4,14]]},"DOI":"10.1145\/3644033.3644374","type":"proceedings-article","created":{"date-parts":[[2024,6,6]],"date-time":"2024-06-06T16:56:27Z","timestamp":1717692987000},"page":"138-142","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Leveraging Large Language Models to Boost Dafny\u2019s Developers Productivity"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-2941-9942","authenticated-orcid":false,"given":"\u00c1lvaro F.","family":"Silva","sequence":"first","affiliation":[{"name":"Independent Researcher, Porto, Portugal"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8060-5920","authenticated-orcid":false,"given":"Alexandra","family":"Mendes","sequence":"additional","affiliation":[{"name":"FEUP, University of Porto and HASLab, INESC TEC, Porto, Portugal"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6612-9013","authenticated-orcid":false,"given":"Jo\u00e3o F.","family":"Ferreira","sequence":"additional","affiliation":[{"name":"INESC-ID and IST, University of Lisbon, Lisbon, Portugal"}]}],"member":"320","published-online":{"date-parts":[[2024,6,6]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASEW60602.2023.00019"},{"key":"e_1_3_2_1_2_1","volume-title":"Specification and Tests. In International Symposium on Leveraging Applications of Formal Methods. Springer, 174--187","author":"Ahrendt Wolfgang","year":"2022","unstructured":"Wolfgang Ahrendt, Dilian Gurov, Moa Johansson, and Philipp R\u00fcmmer. 2022. TriCo---Triple Co-piloting of Implementation, Specification and Tests. In International Symposium on Leveraging Applications of Formal Methods. Springer, 174--187."},{"key":"e_1_3_2_1_3_1","volume-title":"GPT-4 Technical report. arXiv preprint arXiv:2303.08774","author":"Open AI.","year":"2023","unstructured":"Open AI. 2023. GPT-4 Technical report. arXiv preprint arXiv:2303.08774 (2023)."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Lasse Blaauwbroek Josef Urban and Herman Geuvers. 2020. The Tactician. In Intelligent Computer Mathematics. 271--277.","DOI":"10.1007\/978-3-030-53518-6_17"},{"key":"e_1_3_2_1_5_1","volume-title":"Yuanzhi Li, Scott Lundberg, et al.","author":"Bubeck S\u00e9bastien","year":"2023","unstructured":"S\u00e9bastien Bubeck, Varun Chandrasekaran, Ronen Eldan, Johannes Gehrke, Eric Horvitz, Ece Kamar, Peter Lee, Yin Tat Lee, Yuanzhi Li, Scott Lundberg, et al. 2023. Sparks of artificial general intelligence: Early experiments with gpt-4. arXiv preprint arXiv:2303.12712 (2023)."},{"key":"e_1_3_2_1_6_1","volume-title":"24th International Symposium on Formal Methods (FM) (LNCS","volume":"462","author":"Cassez Franck","year":"2021","unstructured":"Franck Cassez. 2021. Verification of the incremental Merkle tree algorithm with Dafny. In 24th International Symposium on Formal Methods (FM) (LNCS, Vol. 13047). Springer, 445--462."},{"key":"e_1_3_2_1_7_1","volume-title":"Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny. In International Symposium on Formal Methods. Springer, 571--583","author":"Cassez Franck","year":"2023","unstructured":"Franck Cassez, Joanne Fuller, Milad K Ghale, David J Pearce, and Horacio MA Quiles. 2023. Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny. In International Symposium on Formal Methods. Springer, 571--583."},{"key":"e_1_3_2_1_8_1","volume-title":"International Conference on Formal Methods for Industrial Critical Systems. Springer, 50--66","author":"Cassez Franck","year":"2022","unstructured":"Franck Cassez, Joanne Fuller, and Horacio Mijail Ant\u00f3n Quiles. 2022. Deductive verification of smart contracts with Dafny. In International Conference on Formal Methods for Industrial Critical Systems. Springer, 50--66."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3464971.3468422"},{"key":"e_1_3_2_1_11_1","volume-title":"2009 39th IEEE Frontiers in Education Conference. IEEE, 1--6.","author":"Ferreira Jo\u00e3o F","year":"2009","unstructured":"Jo\u00e3o F Ferreira and Alexandra Mendes. 2009. Students' feedback on teaching mathematics through the calculational method. In 2009 39th IEEE Frontiers in Education Conference. IEEE, 1--6."},{"key":"e_1_3_2_1_12_1","volume-title":"Teaching Formal Methods: Second International Conference, TFM 2009, Eindhoven, The Netherlands, November 2--6, 2009. Proceedings 2. Springer, 39--56","author":"Ferreira Joao F","year":"2009","unstructured":"Joao F Ferreira, Alexandra Mendes, Roland Backhouse, and Luis S Barbosa. 2009. Which mathematics for the information society?. In Teaching Formal Methods: Second International Conference, TFM 2009, Eindhoven, The Netherlands, November 2--6, 2009. Proceedings 2. Springer, 39--56."},{"key":"e_1_3_2_1_13_1","volume-title":"Tools for Teaching Logic: Third International Congress, TICTTL 2011, Salamanca, Spain, June 1--4, 2011. Proceedings. Springer, 62--69","author":"Ferreira Joao F","year":"2011","unstructured":"Joao F Ferreira, Alexandra Mendes, Alcino Cunha, Carlos Baquero, and Paulo Silva. 2011. Logic training through algorithmic problem solving. In Tools for Teaching Logic: Third International Congress, TICTTL 2011, Salamanca, Spain, June 1--4, 2011. Proceedings. Springer, 62--69."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510003.3510138"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428299"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616243"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3522674"},{"key":"e_1_3_2_1_18_1","unstructured":"Daniel Huang Prafulla Dhariwal Dawn Song and Ilya Sutskever. 2019. GamePad: A Learning Environment for Theorem Proving. In ICLR. https:\/\/openreview.net\/forum?id=r1xwKoR9Y7"},{"key":"e_1_3_2_1_19_1","volume-title":"Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers. In NeurIPS.","author":"Jiang Albert","year":"2022","unstructured":"Albert Jiang, Konrad Czechowski, Mateja Jamnik, Piotr Milos, Szymon Tworkowski, Wenda Li, and Yuhuai Tony Wu. 2022. Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers. In NeurIPS."},{"key":"e_1_3_2_1_20_1","volume-title":"Inferfix: End-to-end program repair with llms. arXiv preprint arXiv:2303.07263","author":"Jin Matthew","year":"2023","unstructured":"Matthew Jin, Syed Shahriar, Michele Tufano, Xin Shi, Shuai Lu, Neel Sundaresan, and Alexey Svyatkovskiy. 2023. Inferfix: End-to-end program repair with llms. arXiv preprint arXiv:2303.07263 (2023)."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3551349.3559548"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_3_2_1_23_1","unstructured":"K Rustan M Leino. 2023. Program Proofs. MIT Press."},{"key":"e_1_3_2_1_24_1","volume-title":"Working Conference on Verified Software: Theories, Tools, and Experiments. Springer, 170--190","author":"Leino K Rustan M","year":"2013","unstructured":"K Rustan M Leino and Nadia Polikarpova. 2013. Verified calculations. In Working Conference on Verified Software: Theories, Tools, and Experiments. Springer, 170--190."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3376127"},{"key":"e_1_3_2_1_26_1","volume-title":"Proceedings of the Ninth ACM International Conference on Interactive Tabletops and Surfaces. 139--148","author":"Mendes Alexandra","year":"2014","unstructured":"Alexandra Mendes, Roland Backhouse, and Joao F Ferreira. 2014. Structure editing of handwritten mathematics: Improving the computer support for the calculational method. In Proceedings of the Ninth ACM International Conference on Interactive Tabletops and Surfaces. 139--148."},{"key":"e_1_3_2_1_27_1","volume-title":"Interactive Theorem Proving: 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9--12, 2018, Proceedings 9. Springer, 432--440","author":"Mendes Alexandra","year":"2018","unstructured":"Alexandra Mendes and Joao F Ferreira. 2018. Towards Verified Handwritten Calculational Proofs: (Short Paper). In Interactive Theorem Proving: 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9--12, 2018, Proceedings 9. Springer, 432--440."},{"key":"e_1_3_2_1_28_1","volume-title":"Jin Peng Zhou, Christian Szegedy, \u0141ukasz Kuci\u0144ski, Piotr Milo\u015b, and Yuhuai Wu.","author":"Mikula Maciej","year":"2023","unstructured":"Maciej Mikula, Szymon Antoniak, Szymon Tworkowski, Albert Qiaochu Jiang, Jin Peng Zhou, Christian Szegedy, \u0141ukasz Kuci\u0144ski, Piotr Milo\u015b, and Yuhuai Wu. 2023. Magnushammer: A Transformer-based Approach to Premise Selection. arXiv:2303.04488"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3524842.3528470"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3524459.3527351"},{"key":"e_1_3_2_1_31_1","volume-title":"14th International Conference on Interactive Theorem Proving (ITP","author":"Reichel Tom","year":"2023","unstructured":"Tom Reichel, R Henderson, Andrew Touchet, Andrew Gardner, and Talia Ringer. 2023. Proof repair infrastructure for supervised models: Building a large proof repair dataset. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Schloss-Dagstuhl-Leibniz Zentrum f\u00fcr Informatik."},{"key":"e_1_3_2_1_32_1","volume-title":"Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages. 1--10","author":"Sanchez-Stern Alex","year":"2020","unstructured":"Alex Sanchez-Stern, Yousef Alhessi, Lawrence Saul, and Sorin Lerner. 2020. Generating correctness proofs with neural networks. In Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages. 1--10."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3593374"},{"key":"e_1_3_2_1_34_1","volume-title":"Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+. In 2022 Formal Methods in Computer-Aided Design (FMCAD)","author":"Schultz William","unstructured":"William Schultz, Ian Dardik, and Stavros Tripakis. 2022. Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+. In 2022 Formal Methods in Computer-Aided Design (FMCAD). IEEE, 273--283."},{"key":"e_1_3_2_1_35_1","volume-title":"Proceedings of the ACM on Programming Languages 6, OOPSLA2","author":"Sivaraman Aishwarya","year":"2022","unstructured":"Aishwarya Sivaraman, Alex Sanchez-Stern, Bretton Chen, Sorin Lerner, and Todd Millstein. 2022. Data-driven lemma synthesis for interactive proofs. Proceedings of the ACM on Programming Languages 6, OOPSLA2 (2022), 505--531."},{"key":"e_1_3_2_1_36_1","volume-title":"Clover: Closed-Loop Verifiable Code Generation. arXiv preprint arXiv:2310.17807","author":"Sun Chuyue","year":"2023","unstructured":"Chuyue Sun, Ying Sheng, Oded Padon, and Clark Barrett. 2023. Clover: Closed-Loop Verifiable Code Generation. arXiv preprint arXiv:2310.17807 (2023)."},{"key":"e_1_3_2_1_37_1","volume-title":"Proceedings of the ACM on Programming Languages 2, POPL","author":"Ta Quang-Trung","year":"2017","unstructured":"Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin. 2017. Automated lemma synthesis in symbolic-heap separation logic. Proceedings of the ACM on Programming Languages 2, POPL (2017), 1--29."},{"key":"e_1_3_2_1_38_1","unstructured":"Amitayush Thakur Yeming Wen and Swarat Chaudhuri. 2023. A Language-Agent Approach to Formal Theorem-Proving. arXiv:2310.04353"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2020.3011744"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00129"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3540250.3549101"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2017.2734091"},{"key":"e_1_3_2_1_43_1","unstructured":"Kaiyu Yang and Jia Deng. 2019. Learning to prove theorems via interacting with proof assistants. In ICML. 6984--6994."},{"key":"e_1_3_2_1_44_1","unstructured":"Kaiyu Yang Aidan Swope Alex Gu Rahul Chalamala Peiyang Song Shixing Yu Saad Godil Ryan Prenger and Anima Anandkumar. 2023. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. In Neural Information Processing Systems (NeurIPS)."},{"key":"e_1_3_2_1_45_1","volume-title":"Principles and Practice of Constraint Programming: 25th International Conference, CP 2019, Stamford, CT, USA, September 30--October 4, 2019, Proceedings 25","author":"Yang Weikun","year":"2019","unstructured":"Weikun Yang, Grigory Fedyukovich, and Aarti Gupta. 2019. Lemma synthesis for automating induction over algebraic data types. In Principles and Practice of Constraint Programming: 25th International Conference, CP 2019, Stamford, CT, USA, September 30--October 4, 2019, Proceedings 25. Springer, 600--617."}],"event":{"name":"FormaliSE '24: 2024 IEEE\/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE)","location":"Lisbon Portugal","acronym":"FormaliSE '24","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"]},"container-title":["Proceedings of the 2024 IEEE\/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE)"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3644033.3644374","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3644033.3644374","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T23:56:58Z","timestamp":1750291018000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3644033.3644374"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,14]]},"references-count":45,"alternative-id":["10.1145\/3644033.3644374","10.1145\/3644033"],"URL":"https:\/\/doi.org\/10.1145\/3644033.3644374","relation":{},"subject":[],"published":{"date-parts":[[2024,4,14]]},"assertion":[{"value":"2024-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}