:: Library Catalog

Cover Image

Saved in:

Bibliographic Details
Main Authors:	Liu, Chang, Wu, Xiwei, Feng, Yuan, Cao, Qinxiang, Yan, Junchi
Format:	Preprint
Published:	2023
Subjects:	Programming Languages
Online Access:	https://arxiv.org/abs/2311.10483
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic
by: Wu, Shushu, et al.
Published: (2025)

A Coq Library of Sets for Teaching Denotational Semantics
by: Cao, Qinxiang, et al.
Published: (2024)

A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms
by: Yang, Chengxi, et al.
Published: (2025)

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

Stellis: A Strategy Language for Purifying Separation Logic Entailments
by: Wang, Zhiyi, et al.
Published: (2025)

A Natural Formalized Proof Language
by: Xie, Lihan, et al.
Published: (2024)

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

QCP: A Practical Separation Logic-based C Program Verification Tool
by: Wu, Xiwei, et al.
Published: (2025)

Denotation-based Compositional Compiler Verification
by: Cheng, Zhang, et al.
Published: (2024)

Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving
by: Liu, Qi, et al.
Published: (2025)

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

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

PPM: Automated Generation of Diverse Programming Problems for Benchmarking Code Generation Models
by: Chen, Simin, et al.
Published: (2024)

C*: Unifying Programming and Verification in C
by: Cao, Yiyuan, et al.
Published: (2025)

Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops (Extended Version)
by: Haase, Darion, et al.
Published: (2026)

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

A Neurosymbolic Approach to Loop Invariant Generation via Weakest Precondition Reasoning
by: King, Daragh, et al.
Published: (2025)

Grammar-Aware Literate Generative Mathematical Programming with Compiler-in-the-Loop
by: Rossi, Roberto, et al.
Published: (2026)

Data-Driven Template-Free Invariant Generation
by: Xia, Yuan, et al.
Published: (2023)

Loop Invariant Generation: A Hybrid Framework of Reasoning optimised LLMs and SMT Solvers
by: Bharti, Varun, et al.
Published: (2025)

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

Neuro-Symbolic Generation and Validation of Memory-Aware Formal Function Specifications
by: Zhang, Liao, et al.
Published: (2026)

LoopSCC: Towards Summarizing Multi-branch Loops within Determinate Cycles
by: Zhu, Kai, et al.
Published: (2024)

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

JavaBench: A Benchmark of Object-Oriented Code Generation for Evaluating Large Language Models
by: Cao, Jialun, et al.
Published: (2024)

Towards General-Purpose Data Discovery: A Programming Languages Approach
by: Kang, Andrew, et al.
Published: (2025)

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

Algebraic Tools for Computing Polynomial Loop Invariants
by: Bayarmagnai, Erdenebayar, et al.
Published: (2024)

Synthesizing Invariants for Polynomial Programs by Semidefinite Programming
by: Wu, Hao, et al.
Published: (2023)

Benchmarking LLM Code Generation for Audio Programming with Visual Dataflow Languages
by: Zhang, William, et al.
Published: (2024)

CodeARC: Benchmarking Reasoning Capabilities of LLM Agents for Inductive Program Synthesis
by: Wei, Anjiang, et al.
Published: (2025)

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

Algebraic and Algorithmic Methods for Computing Polynomial Loop Invariants
by: Bayarmagnai, Erdenebayar, et al.
Published: (2024)

Resource Specifications for Resource-Manipulating Programs
by: Grannan, Zachary, et al.
Published: (2023)

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

Generative Explanations for Program Synthesizers
by: Nazari, Amirmohammad, et al.
Published: (2024)

Strengthening Solidity Invariant Generation: From Post- to Pre-Deployment
by: Kaushik, Kartik, et al.
Published: (2024)

Optimising Density Computations in Probabilistic Programs via Automatic Loop Vectorisation
by: Lim, Sangho, et al.
Published: (2025)

Flex Attention: A Programming Model for Generating Optimized Attention Kernels
by: Dong, Juechu, et al.
Published: (2024)

Static Factorisation of Probabilistic Programs With User-Labelled Sample Statements and While Loops
by: Böck, Markus, et al.
Published: (2025)