{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T19:38:40Z","timestamp":1773171520233,"version":"3.50.1"},"reference-count":36,"publisher":"IEEE","license":[{"start":{"date-parts":[[2025,3,31]],"date-time":"2025-03-31T00:00:00Z","timestamp":1743379200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2025,3,31]],"date-time":"2025-03-31T00:00:00Z","timestamp":1743379200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,3,31]]},"DOI":"10.1109\/icst62969.2025.10989026","type":"proceedings-article","created":{"date-parts":[[2025,5,20]],"date-time":"2025-05-20T17:05:21Z","timestamp":1747760721000},"page":"542-552","source":"Crossref","is-referenced-by-count":1,"title":["Accessible Smart Contracts Verification: Synthesizing Formal Models with Tamed LLMs"],"prefix":"10.1109","author":[{"given":"Jan","family":"Corazza","sequence":"first","affiliation":[{"name":"TU Dortmund University,Research Center Trustworthy Data Science and Security,Dortmund,Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ivan","family":"Gavran","sequence":"additional","affiliation":[{"name":"Informal Systems,Vienna,Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gabriela","family":"Moreira","sequence":"additional","affiliation":[{"name":"Informal Systems,Joinville,Brazil"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Neider","sequence":"additional","affiliation":[{"name":"TU Dortmund University,Research Center Trustworthy Data Science and Security,Dortmund,Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/1353673.1353681"},{"key":"ref2","volume-title":"Cosmwasm book"},{"key":"ref3","volume-title":"Quint"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"ref5","volume-title":"Cosmwasm capture the flag competition tasks"},{"key":"ref6","volume-title":"Jepsen"},{"key":"ref7","volume-title":"Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport","year":"2002"},{"key":"ref8","volume-title":"Tla+ ibc specifications"},{"key":"ref9","volume-title":"Reference implementation of eth2.0 in dafny"},{"issue":"6","key":"ref10","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1109\/MS.2017.4121212","article-title":"Accessible software verification with dafny","volume":"34","author":"Leino","year":"2017","journal-title":"IEEE Softw."},{"key":"ref11","volume-title":"Certora prover"},{"key":"ref12","volume-title":"Slither code repository"},{"key":"ref13","volume-title":"Mythril code repository"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/3460319.3469076"},{"key":"ref15","volume-title":"Kontrol code repository"},{"key":"ref17","article-title":"Evaluating large language models trained on code","volume":"abs\/2107.03374","author":"Chen","year":"2021","journal-title":"CoRR"},{"key":"ref18","article-title":"Code llama: Open foundation models for code","volume":"abs\/2308.12950","author":"Roziere","year":"2023","journal-title":"CoRR"},{"key":"ref19","article-title":"PICARD: parsing incrementally for constrained auto-regressive decoding from language models","volume":"abs\/2109.05093","author":"Scholak","year":"2021","journal-title":"CoRR"},{"key":"ref20","article-title":"Synchromesh: Reliable code generation from pre-trained language models","volume-title":"International Conference on Learning Representations","author":"Poesia"},{"key":"ref21","author":"Sun","year":"2024","journal-title":"Clover: Closed-loop verifiable code generation"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/3650212.3680347"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2024.24556"},{"key":"ref24","article-title":"A new era in software security: Towards self-healing software via large language models and formal verification","author":"Charalambous","year":"2023","journal-title":"arXiv preprint"},{"key":"ref25","article-title":"Optimal neural program synthesis from multimodal specifications","author":"Ye","year":"2020","journal-title":"arXiv preprint"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/3510003.3510203"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/3643763"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2024.emnlp-main.667"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48153-2_6"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1145\/3360549"},{"key":"ref31","volume-title":"Software Abstractions: logic, language, and analysis","author":"Jackson","year":"2012"},{"key":"ref32","author":"Corazza","year":"2025","journal-title":"Accessible smart contracts verification: Synthesizing formal models with tamed llms"},{"key":"ref33","volume-title":"Rustc plugin"},{"key":"ref34","volume-title":"cw-multi-test cosmwasm testing framework"},{"key":"ref35","article-title":"Language models are few-shot learners","volume":"abs\/2005.14165","author":"Brown","year":"2020","journal-title":"CoRR"},{"key":"ref36","article-title":"Chain of thought prompting elicits reasoning in large language models","volume":"abs\/2201.11903","author":"Wei","year":"2022","journal-title":"CoRR"},{"key":"ref37","volume-title":"Neutron github org"}],"event":{"name":"2025 IEEE Conference on Software Testing, Verification and Validation (ICST)","location":"Napoli, Italy","start":{"date-parts":[[2025,3,31]]},"end":{"date-parts":[[2025,4,4]]}},"container-title":["2025 IEEE Conference on Software Testing, Verification and Validation (ICST)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/10988917\/10988918\/10989026.pdf?arnumber=10989026","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T05:50:49Z","timestamp":1747806649000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10989026\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,31]]},"references-count":36,"URL":"https:\/\/doi.org\/10.1109\/icst62969.2025.10989026","relation":{},"subject":[],"published":{"date-parts":[[2025,3,31]]}}}