@article{2025arXiv251220486C,
    author = {Ştefan Ciobâcă and K. Rustan M. Leino and Ştefan-Alexandru Mercatextcommabelow s and Roxana-Mihaela Timon},
    doi = {https://dx.doi.org/10.48550/arxiv.2512.20486},
    title = {{The Design of an Interactive Proof Mode for Dafny}},
    journal = {arXiv e-prints},
    year = {2025},
    month = {dec},
    eid = {arXiv:2512.20486},
    pages = {arXiv:2512.20486},
    archiveprefix = {arXiv},
    eprint = {2512.20486},
    primaryclass = {cs.LO},
    adsurl = {https://ui.adsabs.harvard.edu/abs/2025arXiv251220486C},
    adsnote = {Provided by the SAO/NASA Astrophysics Data System},
    date-added = {2025-12-29 13:17:21 +0100},
    nextcloud = {https://yossarian.ddns.net:4843/nextcloud/index.php/apps/files/files?dir=/Library/bibliographer/./library/entries/2025arXiv251220486C/},
    date-modified = {2026-1-5 15:40:17 +0100}
}

@article{2025arXiv251220486C, author = {Ştefan Ciobâcă and K. Rustan M. Leino and Ştefan-Alexandru Mercatextcommabelow s and Roxana-Mihaela Timon}, doi = {https://dx.doi.org/10.48550/arxiv.2512.20486}, title = {{The Design of an Interactive Proof Mode for Dafny}}, journal = {arXiv e-prints}, year = {2025}, month = {dec}, eid = {arXiv:2512.20486}, pages = {arXiv:2512.20486}, archiveprefix = {arXiv}, eprint = {2512.20486}, primaryclass = {cs.LO}, adsurl = {https://ui.adsabs.harvard.edu/abs/2025arXiv251220486C}, adsnote = {Provided by the SAO/NASA Astrophysics Data System}, date-added = {2025-12-29 13:17:21 +0100}, nextcloud = {https://yossarian.ddns.net:4843/nextcloud/index.php/apps/files/files?dir=/Library/bibliographer/./library/entries/2025arXiv251220486C/}, date-modified = {2026-1-5 15:40:17 +0100} }