Cover Image

VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Sun, Chuyue, Sun, Yican, Amrollahi, Daneshvar, Zhang, Ethan, Lahiri, Shuvendu, Lu, Shan, Dill, David, Barrett, Clark
Format:	Preprint
Published:	2025
Subjects:	Software Engineering Artificial Intelligence
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

ClassInvGen: Class Invariant Synthesis using Large Language Models
by: Sun, Chuyue, et al.
Published: (2025)

AutoVerus: Automated Proof Generation for Rust Code
by: Yang, Chenyuan, et al.
Published: (2024)

Faithful Autoformalization via Roundtrip Verification and Repair
by: Amrollahi, Daneshvar, et al.
Published: (2026)

Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages
by: Lahiri, Shuvendu K.
Published: (2024)

Program Structure Aware Precondition Generation
by: Dinella, Elizabeth, et al.
Published: (2023)

Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents
by: Lahiri, Shuvendu K.
Published: (2026)

Clover: Closed-Loop Verifiable Code Generation
by: Sun, Chuyue, et al.
Published: (2023)

On Reasoning-Centric LLM-based Automated Theorem Proving
by: Sun, Yican, et al.
Published: (2026)

3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers
by: Fakhoury, Sarah, et al.
Published: (2024)

RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation
by: Zhong, Sicheng, 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)

LLM-Based Test-Driven Interactive Code Generation: User Study and Empirical Evaluation
by: Fakhoury, Sarah, et al.
Published: (2024)

Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?
by: Endres, Madeline, et al.
Published: (2023)

VeriODD: From YAML to SMT-LIB -- Automating Verification of Operational Design Domains
by: Rafie, Bassel, et al.
Published: (2025)

Automated Proof Generation for Rust Code via Self-Evolution
by: Chen, Tianyu, et al.
Published: (2024)

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

LLM-Vectorizer: LLM-based Verified Loop Vectorizer
by: Taneja, Jubi, et al.
Published: (2024)

GramTrans: A Better Code Representation Approach in Code Generation
by: Zhang, Zhao, et al.
Published: (2025)

Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization
by: Agarwal, Anmol, et al.
Published: (2026)

StructCoder: Structure-Aware Transformer for Code Generation
by: Tipirneni, Sindhu, et al.
Published: (2022)

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

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

StructEval: Benchmarking LLMs' Capabilities to Generate Structural Outputs
by: Yang, Jialin, et al.
Published: (2025)

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

ExVerus: Verus Proof Repair via Counterexample Reasoning
by: Yang, Jun, et al.
Published: (2026)

A Multi-Year Grey Literature Review on AI-assisted Test Automation
by: Ricca, Filippo, et al.
Published: (2024)

Formalizing UML State Machines for Automated Verification -- A Survey
by: André, Étienne, et al.
Published: (2024)

Automating Business Intelligence Requirements with Generative AI and Semantic Search
by: Busany, Nimrod, et al.
Published: (2024)

Automated Repair of AI Code with Large Language Models and Formal Verification
by: Charalambous, Yiannis, et al.
Published: (2024)

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

BitsAI-CR: Automated Code Review via LLM in Practice
by: Sun, Tao, et al.
Published: (2025)

Visualisation and Automated Formal Verification of TOSCA Workflows
by: Ouadie Khebbeb, et al.
Published: (2026)

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

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

SLA-Awareness for AI-assisted coding
by: Thangarajah, Kishanthan, et al.
Published: (2025)

VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean
by: Xin, Yutong, et al.
Published: (2026)

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

An Encoding for CLP Problems in SMT-LIB
by: Amrollahi, Daneshvar, et al.
Published: (2024)

Codexity: Secure AI-assisted Code Generation
by: Kim, Sung Yong, et al.
Published: (2024)

Automating Formal Verification with Reinforcement Learning and Recursive Inference
by: Tan, Max
Published: (2026)