Cover Image

DafnyPro: LLM-Assisted Automated Verification for Dafny Programs

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Banerjee, Debangshu, Bouissou, Olivier, Zetzsche, Stefan
Format:	Preprint
Published:	2026
Subjects:	Software Engineering
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Dafny as Verification-Aware Intermediate Language for Code Generation
by: Li, Yue Chen, et al.
Published: (2025)

dafny-annotator: AI-Assisted Verification of Dafny Programs
by: Poesia, Gabriel, et al.
Published: (2024)

MutDafny: A Mutation-Based Approach to Assess Dafny Specifications
by: Amaral, Isabel, et al.
Published: (2025)

Towards AI-Assisted Synthesis of Verified Dafny Methods
by: Misu, Md Rakib Hossain, et al.
Published: (2024)

ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis
by: Baksys, Mantas, et al.
Published: (2025)

DafnyBench: A Benchmark for Formal Software Verification
by: Loughridge, Chloe, et al.
Published: (2024)

Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs
by: Wu, Valentina, et al.
Published: (2025)

From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification
by: Erfan, Md, et al.
Published: (2026)

Teaching LLMs Program Semantics via Symbolic Execution Traces
by: Bayer, Jonas, et al.
Published: (2026)

Inferring multiple helper Dafny assertions with LLMs
by: Silva, Álvaro, et al.
Published: (2025)

Leveraging Large Language Models to Boost Dafny's Developers Productivity
by: Silva, Álvaro, et al.
Published: (2024)

Can Large Language Models Help Students Prove Software Correctness? An Experimental Study with Dafny
by: Carreira, Carolina, et al.
Published: (2025)

Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny
by: Zetzsche, Stefan, et al.
Published: (2024)

Verifying the Fisher-Yates Shuffle Algorithm in Dafny
by: Zetzsche, Stefan, et al.
Published: (2025)

Tunable Automation in Automated Program Verification
by: Bai, Alexander Y., et al.
Published: (2025)

LLM-Assisted Tool for Joint Generation of Formulas and Functions in Rule-Based Verification of Map Transformations
by: He, Ruidi, et al.
Published: (2025)

SpecSyn: LLM-based Synthesis and Refinement of Formal Specifications for Real-world Program Verification
by: Ma, Lezhi, et al.
Published: (2026)

Semantic Evolution over Populations for LLM-Guided Automated Program Repair
by: Le, Cuong Chi, et al.
Published: (2026)

Lemma Discovery in Agentic Program Verification
by: Zhao, Huan, et al.
Published: (2026)

Selene: Pioneering Automated Proof in Software Verification
by: Zhang, Lichen, et al.
Published: (2024)

HEJ-Robust: A Robustness Benchmark for LLM-Based Automated Program Repair
by: Rabbi, Fazle, et al.
Published: (2026)

Exploring and Lifting the Robustness of LLM-powered Automated Program Repair with Metamorphic Testing
by: Xue, Pengyu, et al.
Published: (2024)

Automating Execution and Verification of BPMN+DMN Business Processes
by: Della Penna, Giuseppe, et al.
Published: (2025)

DINGO: Constrained Inference for Diffusion LLMs
by: Suresh, Tarun, et al.
Published: (2025)

Leveraging Mutation Analysis for LLM-based Repair of Quantum Programs
by: Yoshida, Chihiro, et al.
Published: (2026)

A Survey of LLM-based Automated Program Repair: Taxonomies, Design Paradigms, and Applications
by: Yang, Boyang, et al.
Published: (2025)

UVMarvel: an Automated LLM-aided UVM Machine for Subsystem-level RTL Verification
by: Ye, Junhao, et al.
Published: (2026)

DePro: Understanding the Role of LLMs in Debugging Competitive Programming Code
by: Parvez, Nabiha, et al.
Published: (2026)

The Impact of Program Reduction on Automated Program Repair
by: Vidziunas, Linas, et al.
Published: (2024)

Scalable Deductive Verification of Data-Level Parallel Programs
by: Haak, Lars B. van den, et al.
Published: (2026)

DebugRepair: Enhancing LLM-Based Automated Program Repair via Self-Directed Debugging
by: Wu, Linhao, et al.
Published: (2026)

You Can REST Now: Automated REST API Documentation and Testing via LLM-Assisted Request Mutations
by: Decrop, Alix, et al.
Published: (2024)

Agents4PLC: Automating Closed-loop PLC Code Generation and Verification in Industrial Control Systems using LLM-based Agents
by: Liu, Zihan, et al.
Published: (2024)

Logic Mining from Process Logs: Towards Automated Specification and Verification
by: Klimek, Radoslaw, et al.
Published: (2025)

ProDebug: An Automated Debugging System for Prolog
by: Brancas, Ricardo, et al.
Published: (2026)

LLM4VV: Exploring LLM-as-a-Judge for Validation and Verification Testsuites
by: Sollenberger, Zachariah, et al.
Published: (2024)

Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification
by: Wen, Cheng, et al.
Published: (2024)

Specification Vibing for Automated Program Repair
by: Zhu, Taohong, et al.
Published: (2026)

Energy Consumption of Automated Program Repair
by: Martinez, Matias, et al.
Published: (2022)

AUTOGENICS: Automated Generation of Context-Aware Inline Comments for Code Snippets on Programming Q&A Sites Using LLM
by: Bappon, Suborno Deb, et al.
Published: (2024)