Cover Image

Ranking LLM-Generated Loop Invariants for Program Verification

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Chakraborty, Saikat, Lahiri, Shuvendu K., Fakhoury, Sarah, Musuvathi, Madanlal, Lal, Akash, Rastogi, Aseem, Senthilnathan, Aditya, Sharma, Rahul, Swamy, Nikhil
Format:	Preprint
Published:	2023
Subjects:	Programming Languages Artificial Intelligence Computation and Language Software Engineering
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

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

Enabling Memory Safety of C Programs using LLMs
by: Mohammed, Nausheen, et al.
Published: (2024)

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)

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

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

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

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

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

Automatically Verifying Replication-aware Linearizability
by: Soundarapandian, Vimala, et al.
Published: (2025)

Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis
by: Wei, Anjiang, et al.
Published: (2025)

Towards General Loop Invariant Generation: A Benchmark of Programs with Memory Manipulation
by: Liu, Chang, et al.
Published: (2023)

Parameterized Verification of Timed Networks with Clock Invariants
by: André, Étienne, et al.
Published: (2024)

Knowledge Planning in Large Language Models for Domain-Aligned Counseling Summarization
by: Srivastava, Aseem, et al.
Published: (2024)

Open-Loop Planning, Closed-Loop Verification: Speculative Verification for VLA
by: Wang, Zihua, et al.
Published: (2026)

Trust Modeling in Counseling Conversations: A Benchmark Study
by: Srivastava, Aseem, et al.
Published: (2025)

Towards Automated Verification of LLM-Synthesized C Programs
by: Mukherjee, Prasita, et al.
Published: (2024)

Guiding LLM-based Loop Invariant Synthesis via Feedback on Local Reasoning Errors
by: Li, Tianchi, et al.
Published: (2026)

Sentiment-guided Commonsense-aware Response Generation for Mental Health Counseling
by: Srivastava, Aseem, et al.
Published: (2025)

CIR+CVN: Bridging LLM Semantic Understanding and Petri-Net Verification for Concurrent Programs
by: Zhang, Kaiwen, et al.
Published: (2026)

Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE
by: Ramananandro, Tahina, et al.
Published: (2025)

Probabilistic Guarantees for Practical LIA Loop Invariant Automation
by: Kumar, Ashish, et al.
Published: (2024)

Analyzing LLM Instruction Optimization for Tabular Fact Verification
by: Du, Xiaotang, et al.
Published: (2026)

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

Few-Shot Fairness: Unveiling LLM's Potential for Fairness-Aware Classification
by: Chhikara, Garima, et al.
Published: (2024)

An Empirical Evaluation of Encoder Architectures for Fast Real-Time Long Conversational Understanding
by: Senthilnathan, Annamalai, et al.
Published: (2025)

Prompt Compression with Context-Aware Sentence Encoding for Fast and Improved LLM Inference
by: Liskavets, Barys, et al.
Published: (2024)

User-Centric Evidence Ranking for Attribution and Fact Verification
by: Alt, Guy, et al.
Published: (2026)

ParamBench: A Graduate-Level Benchmark for Evaluating LLM Understanding on Indic Subjects
by: Maheshwari, Ayush, et al.
Published: (2025)

BALI: Branch-Aware Loop Invariant Inference with Large Language Models
by: Wang, Mingxiu, et al.
Published: (2025)

Linguistic Loops and Geometric Invariants as a Way to Pre-Verbal Thought?
by: Corradetti, Daniele, et al.
Published: (2025)

SciClaimHunt: A Large Dataset for Evidence-based Scientific Claim Verification
by: Kumar, Sujit, et al.
Published: (2025)

SpecLoop: An Agentic RTL-to-Specification Framework with Formal Verification Feedback Loop
by: Chang, Fu-Chieh, et al.
Published: (2026)

MuSciClaims: Multimodal Scientific Claim Verification
by: Lal, Yash Kumar, et al.
Published: (2025)

Practical Formal Verification for MLIR Programs
by: Tucker, Emily, et al.
Published: (2026)

MultiCheck: Strengthening Web Trust with Unified Multimodal Fact Verification
by: Kishore, Aditya, et al.
Published: (2025)

Deduplicating and Ranking Solution Programs for Suggesting Reference Solutions
by: Shirafuji, Atsushi, et al.
Published: (2023)

Data-Driven Invariant Learning for Probabilistic Programs
by: Bao, Jialu, et al.
Published: (2021)

Polynomial Invariant Generation for Floating-Point Programs
by: Cai, Xuran, et al.
Published: (2025)