{"total":44,"rows":[{"id":"2406.08467","title":"DafnyBench: A Benchmark for Formal Software Verification","created":"2024-06-12","cited_by_count":57,"area":null},{"id":"2409.13082","title":"AutoVerus: Automated Proof Generation for Rust Code","created":"2024-09-19","cited_by_count":49,"area":null},{"id":"2505.23135","title":"VERINA: Benchmarking Verifiable Code Generation","created":"2025-05-29","cited_by_count":34,"area":null},{"id":"2410.15756","title":"Automated Proof Generation for Rust Code via Self-Evolution","created":"2024-10-21","cited_by_count":33,"area":null},{"id":"2405.01787","title":"Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming","created":"2024-05-03","cited_by_count":20,"area":null},{"id":"2502.05714","title":"Proving the Coding Interview: A Benchmark for Formally Verified Code Generation","created":"2025-02-08","cited_by_count":19,"area":null},{"id":"2508.16546","title":"RL Is Neither a Panacea Nor a Mirage: Understanding Supervised vs. Reinforcement Learning Fine-Tuning for LLMs","created":"2025-08-22","cited_by_count":17,"area":null},{"id":"2602.09464","title":"AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms","created":"2026-02-10","cited_by_count":12,"area":null},{"id":"2405.16792","title":"Laurel: Unblocking Automated Verification with Large Language Models","created":"2024-05-27","cited_by_count":11,"area":null},{"id":"2510.25015","title":"VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus","created":"2025-10-28","cited_by_count":9,"area":null},{"id":"2504.20964","title":"OSVBench: Benchmarking LLMs on Specification Generation Tasks for Operating System Verification","created":"2025-04-29","cited_by_count":8,"area":null},{"id":"2406.10903","title":"New Solutions on LLM Acceleration, Optimization, and Application","created":"2024-06-16","cited_by_count":7,"area":null},{"id":"2510.06296","title":"VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code","created":"2025-10-07","cited_by_count":7,"area":null},{"id":"2406.03636","title":"Synthetic Programming Elicitation for Text-to-Code in Very Low-Resource Programming and Formal Languages","created":"2024-06-05","cited_by_count":6,"area":null},{"id":"2501.06283","title":"Dafny as Verification-Aware Intermediate Language for Code Generation","created":"2025-01-10","cited_by_count":6,"area":null},{"id":"2509.23061","title":"Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification","created":"2025-09-27","cited_by_count":6,"area":null},{"id":"2504.11711","title":"The Hitchhiker's Guide to Program Analysis, Part II: Deep Thoughts by LLMs","created":"2025-04-16","cited_by_count":4,"area":null},{"id":"2509.25197","title":"Towards Repository-Level Program Verification with Large Language Models","created":"2025-08-31","cited_by_count":4,"area":null},{"id":"2511.00125","title":"Inferring multiple helper Dafny assertions with LLMs","created":"2025-10-31","cited_by_count":4,"area":null},{"id":"2503.14183","title":"Can LLMs Enable Verification in Mainstream Programming?","created":"2025-03-18","cited_by_count":3,"area":null},{"id":"2604.03758","title":"AutoReSpec: A Framework for Generating Specification using Large Language Models","created":"2026-04-04","cited_by_count":3,"area":null},{"id":"2605.08553","title":"VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation","created":"2026-05-08","cited_by_count":3,"area":null},{"id":"2404.09384","title":"Generative transformations and patterns in LLM-native approaches for software verification and falsification","created":"2024-04-14","cited_by_count":2,"area":null},{"id":"2502.15217","title":"FormalSpecCpp: A Dataset of C++ Formal Specifications created using LLMs","created":"2025-02-21","cited_by_count":2,"area":null},{"id":"2602.04892","title":"Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction","created":"2026-01-30","cited_by_count":2,"area":null},{"id":"2604.00280","title":"Spec-Harness: Assessing and Guiding LLM-Synthesized Formal Specifications Beyond Verifiability","created":"2026-03-31","cited_by_count":2,"area":null},{"id":"2604.10392","title":"Intent-aligned Formal Specification Synthesis via Traceable Refinement","created":"2026-04-12","cited_by_count":2,"area":null},{"id":"2410.18494","title":"Assured Automatic Programming via Large Language Models","created":"2024-10-24","cited_by_count":1,"area":null},{"id":"2506.10998","title":"Towards Automated Formal Verification of Backend Systems with LLMs","created":"2025-04-13","cited_by_count":1,"area":null},{"id":"2511.06552","title":"LLM For Loop Invariant Generation and Fixing: How Far Are We?","created":"2025-11-09","cited_by_count":1,"area":null},{"id":"2512.02080","title":"The 4/$\\delta$ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee","created":"2025-11-30","cited_by_count":1,"area":null},{"id":"2607.04631","title":"Formal Disco: Scalable Open-Ended Generation of Formally Verified Programs","created":"2026-07-06","cited_by_count":1,"area":null},{"id":"2501.05252","title":"From Scientific Texts to Verifiable Code: Automating the Process with Transformers","created":"2025-01-09","cited_by_count":0,"area":null},{"id":"2501.12972","title":"Accessible Smart Contracts Verification: Synthesizing Formal Models with Tamed LLMs","created":"2025-01-22","cited_by_count":0,"area":null},{"id":"2506.14627","title":"Working Document -- Formalising Software Requirements with Large Language Models","created":"2025-06-17","cited_by_count":0,"area":null},{"id":"2512.07501","title":"AutoICE: Automatically Synthesizing Verifiable C Code via LLM-driven Evolution","created":"2025-12-08","cited_by_count":0,"area":null},{"id":"2604.22601","title":"From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification","created":"2026-04-24","cited_by_count":0,"area":null},{"id":"2605.14972","title":"Viverra: Text-to-Code with Guarantees","created":"2026-05-14","cited_by_count":0,"area":null},{"id":"2605.22368","title":"VeriScale: Adversarial Test-Suite Scaling for Verifiable Code Generation","created":"2026-05-21","cited_by_count":0,"area":null},{"id":"2606.26490","title":"An Empirical Study of LLM-Generated Specifications for VeriFast","created":"2026-06-25","cited_by_count":0,"area":null},{"id":"2607.09366","title":"Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiability","created":"2026-07-10","cited_by_count":0,"area":null},{"id":"2609.23954","title":"Djinnlang: Higher-Level Programming by Unambiguous Specification with an LLM in the Compiler","created":"2026-09-21","cited_by_count":0,"area":null},{"id":"2609.34886","title":"Fewer Assumptions by Design: A Reusable Skill for LLM-Assisted Verus Verification","created":"2026-09-28","cited_by_count":0,"area":null},{"id":"2609.39568","title":"Self-Spec Verifiable Code Generation","created":"2026-09-30","cited_by_count":0,"area":null}],"next_cursor":null}