Cover Image

dafny-annotator: AI-Assisted Verification of Dafny Programs

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Poesia, Gabriel, Loughridge, Chloe, Amin, Nada
Format:	Preprint
Published:	2024
Subjects:	Software Engineering Artificial Intelligence Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

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

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

VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search
by: Brandfonbrener, David, et al.
Published: (2024)

Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
by: Chakraborty, Saikat, et al.
Published: (2024)

Natural Language-Oriented Programming (NLOP): Towards Democratizing Software Creation
by: Beheshti, Amin
Published: (2024)

Can LLMs Enable Verification in Mainstream Programming?
by: Shefer, Aleksandr, et al.
Published: (2025)

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

Towards Repository-Level Program Verification with Large Language Models
by: Zhong, Si Cheng, et al.
Published: (2025)

Ranking LLM-Generated Loop Invariants for Program Verification
by: Chakraborty, Saikat, et al.
Published: (2023)

AI-Assisted Fixes to Code Review Comments at Scale
by: Maddila, Chandra, et al.
Published: (2025)

MutDafny: A Mutation-Based Approach to Assess Dafny Specifications
by: Amaral, Isabel, 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)

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

Agentic Proving for Program Verification
by: Sosso, Alessandro, et al.
Published: (2026)

Evaluating the Performance of Large Language Models in Competitive Programming: A Multi-Year, Multi-Grade Analysis
by: Dumitran, Adrian Marius, et al.
Published: (2024)

AI Coders Are Among Us: Rethinking Programming Language Grammar Towards Efficient Code Generation
by: Sun, Zhensu, et al.
Published: (2024)

DafnyPro: LLM-Assisted Automated Verification for Dafny Programs
by: Banerjee, Debangshu, et al.
Published: (2026)

A Problem-Oriented Perspective and Anchor Verification for Code Optimization
by: Ye, Tong, et al.
Published: (2024)

Program Skeletons for Automated Program Translation
by: Wang, Bo, et al.
Published: (2025)

Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification?
by: Richter, Cedric, et al.
Published: (2025)

SACTOR: LLM-Driven Correct and Idiomatic C to Rust Translation with Static Analysis and FFI-Based Verification
by: Zhou, Tianyang, et al.
Published: (2025)

Certified Program Synthesis with a Multi-Modal Verifier
by: Feng, Yueyang, et al.
Published: (2026)

Herb.jl: A Unifying Program Synthesis Library
by: Hinnerichs, Tilman, et al.
Published: (2025)

Stdlib or Third-Party? Empirical Performance and Correctness of LLM-Assisted Zero-Dependency Python Libraries
by: Ding, Peng, et al.
Published: (2026)

Agentic Interpretation: Lattice-Structured Evidence for LLM-Based Program Analysis
by: Mitchell, Jacqueline L., et al.
Published: (2026)

Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models
by: Liu, Ruibang, et al.
Published: (2024)

AbstractBeam: Enhancing Bottom-Up Program Synthesis using Library Learning
by: Zenkner, Janis, et al.
Published: (2024)

Structured Program Synthesis using LLMs: Results and Insights from the IPARC Challenge
by: Surana, Shraddha, et al.
Published: (2025)

AI-Mediated Code Comment Improvement
by: Dhakal, Maria, et al.
Published: (2025)

Static Program Slicing Using Language Models With Dataflow-Aware Pretraining and Constrained Decoding
by: He, Pengfei, et al.
Published: (2026)

Learning to Guarantee Type Correctness in Code Generation through Type-Guided Program Synthesis
by: Huang, Zhechong, et al.
Published: (2025)

Perish or Flourish? A Holistic Evaluation of Large Language Models for Code Generation in Functional Programming
by: Lang, Nguyet-Anh H., et al.
Published: (2026)

Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction
by: Xia, Shihao, et al.
Published: (2026)

Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference
by: Le-Cong, Thanh, et al.
Published: (2025)

Agentic Program Repair from Test Failures at Scale: A Neuro-symbolic approach with static analysis and test execution feedback
by: Maddila, Chandra, et al.
Published: (2025)

From Code Generation to Software Testing: AI Copilot with Context-Based RAG
by: Wang, Yuchen, et al.
Published: (2025)

AutoMCQ -- Automatically Generate Code Comprehension Questions using GenAI
by: Goodfellow, Martin, et al.
Published: (2025)

LLMs Lean on Priors, Not Programming Language Semantics
by: Thimmaiah, Aditya, et al.
Published: (2025)

GitChameleon 2.0: Evaluating AI Code Generation Against Python Library Version Incompatibilities
by: Misra, Diganta, et al.
Published: (2025)