Cover Image

Towards AI-Assisted Synthesis of Verified Dafny Methods

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Misu, Md Rakib Hossain, Lopes, Cristina V., Ma, Iris, Noble, James
Format:	Preprint
Published:	2024
Subjects:	Software Engineering Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

VeriAct: Beyond Verifiability -- Agentic Synthesis of Correct and Complete Formal Specifications
by: Misu, Md Rakib Hossain, et al.
Published: (2026)

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

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)

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)

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

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

AI-Assisted Modeling: DSL-Driven AI Interactions
by: Smyth, Steven, et al.
Published: (2025)

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

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

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

SEVerA: Verified Synthesis of Self-Evolving Agents
by: Banerjee, Debangshu, et al.
Published: (2026)

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

Verifying a Realistic Mutable Hash Table
by: Chassot, Samuel, et al.
Published: (2021)

Verified invertible lexer using regular expressions and DFAs
by: Chassot, Samuel, et al.
Published: (2024)

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

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

Toward Programming Languages for Reasoning: Humans, Symbolic Systems, and AI Agents
by: Marron, Mark
Published: (2024)

Test Smell: A Parasitic Energy Consumer in Software Testing
by: Misu, Md Rakib Hossain, et al.
Published: (2023)

Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study
by: Bucev, Mario, et al.
Published: (2024)

VERT: Verified Equivalent Rust Transpilation with Large Language Models as Few-Shot Learners
by: Yang, Aidan Z. H., et al.
Published: (2024)

From Code to Career: Assessing Competitive Programmers for Industry Placement
by: Akib, Md Imranur Rahman, et al.
Published: (2025)

Toward Automated Validation of Language Model Synthesized Test Cases using Semantic Entropy
by: Taherkhani, Hamed, et al.
Published: (2024)

LLM-Guided Compositional Program Synthesis
by: Khan, Ruhma, et al.
Published: (2025)

Generating Verifiable Chain of Thoughts from Exection-Traces
by: Thakur, Shailja, et al.
Published: (2025)

Towards Analyzing N-language Polyglot Programs
by: Prakash, Jyoti, et al.
Published: (2026)

Towards a Transpiler for C/C++ to Safer Rust
by: Tripuramallu, Dhiren, et al.
Published: (2024)

ReSyn: A Generalized Recursive Regular Expression Synthesis Framework
by: Kim, Seongmin, et al.
Published: (2026)

FlashSyn: Flash Loan Attack Synthesis via Counter Example Driven Approximation
by: Chen, Zhiyang, et al.
Published: (2022)

Embracing Objects Over Statics: An Analysis of Method Preferences in Open Source Java Frameworks
by: Zakharov, Vladimir, et al.
Published: (2024)

The Opaque Pointer Design Pattern in Python: Towards a Pythonic PIMPL for Modularity, Encapsulation, and Stability
by: Saravanos, Antonios, et al.
Published: (2026)

How Natural Language Proficiency Shapes GenAI Code for Software Engineering Tasks
by: Rojpaisarnkit, Ruksit, et al.
Published: (2025)

What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus
by: Jain, Rijul, et al.
Published: (2025)

Scalable, Validated Code Translation of Entire Projects using Large Language Models
by: Zhang, Hanliang, et al.
Published: (2024)

Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-Procedural Path-Sensitive Taint Analysis
by: Ji, Yuchen, et al.
Published: (2025)

Improving the Quality of Commit Messages in Students' Projects
by: Ma, Iris, et al.
Published: (2023)

Rule-Based Error Classification for Analyzing Differences in Frequent Errors
by: Shirafuji, Atsushi, et al.
Published: (2023)

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

Enhancing Python Programming Education with an AI-Powered Code Helper: Design, Implementation, and Impact
by: Amiri, Sayed Mahbub Hasan, et al.
Published: (2025)