Cover Image

(Un)Solvable Loop Analysis

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Amrollahi, Daneshvar, Bartocci, Ezio, Kenison, George, Kovács, Laura, Moosbrugger, Marcel, Stankovič, Miroslav
Format:	Preprint
Published:	2023
Subjects:	Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Polar: An Algebraic Analyzer for (Probabilistic) Loops
by: Moosbrugger, Marcel, et al.
Published: (2026)

Moment-based Invariants for Probabilistic Loops with Non-polynomial Assignments
by: Kofnov, Andrey, et al.
Published: (2022)

Exact and Approximate Moment Derivation for Probabilistic Loops With Non-Polynomial Assignments
by: Kofnov, Andrey, et al.
Published: (2023)

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

Model Checking Probabilistic Operator Precedence Automata
by: Pontiggia, Francesco, et al.
Published: (2024)

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

Linear Loop Synthesis for Quadratic Invariants
by: Hitarth, S., et al.
Published: (2023)

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

Solvable Tuple Patterns and Their Applications to Program Verification
by: Kobayashi, Naoki, et al.
Published: (2025)

Moment-based Density Elicitation with Applications in Probabilistic Loops
by: Kofnov, Andrey, et al.
Published: (2023)

Information-flow Interfaces and Security Lattices
by: Bartocci, Ezio, et al.
Published: (2024)

Fully Symbolic Analysis of Loop Locality: Using Imaginary Reuse to Infer Real Performance
by: Zhu, Yifan, et al.
Published: (2026)

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

A Denotational Semantics for Quantum Loops
by: Assolini, Nicola, et al.
Published: (2025)

The Threshold Problem for Hypergeometric Sequences with Quadratic Parameters
by: Kenison, George
Published: (2022)

Series-Parallel-Loop Decompositions of Control-flow Graphs
by: Cai, Xuran, et al.
Published: (2026)

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

Hypernode Automata
by: Bartocci, Ezio, et al.
Published: (2023)

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

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

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

AutoLALA: Automatic Loop Algebraic Locality Analysis for AI and HPC Kernels
by: Zhu, Yifan, et al.
Published: (2026)

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

Static Factorisation of Probabilistic Programs With User-Labelled Sample Statements and While Loops
by: Böck, Markus, 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)

SparseAuto: An Auto-Scheduler for Sparse Tensor Computations Using Recursive Loop Nest Restructuring
by: Dias, Adhitha, et al.
Published: (2023)

Iterating Pointers: Enabling Static Analysis for Loop-based Pointers
by: Lepori, Andrea, et al.
Published: (2025)

Extracting Protocol Format as State Machine via Controlled Static Loop Analysis
by: Shi, Qingkai, et al.
Published: (2023)

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

Open Source Prover in the Attic
by: Kovács, Zoltán, et al.
Published: (2024)

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

A Tree-Shaped Tableau for Checking the Satisfiability of Signal Temporal Logic with Bounded Temporal Operators
by: Melani, Beatrice, et al.
Published: (2025)

POPACheck: A Model Checker for Probabilistic Pushdown Automata
by: Pontiggia, Francesco, et al.
Published: (2025)

GNU Aris: a web application for students
by: Attri, Saksham, et al.
Published: (2025)

Story of Your Lazy Function's Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs
by: Xia, Li-yao, et al.
Published: (2024)

From Tool Calling to Symbolic Thinking: LLMs in a Persistent Lisp Metaprogramming Loop
by: de la Torre, Jordi
Published: (2025)

MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
by: Leißa, Roland, et al.
Published: (2024)

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

CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses
by: Dobos-Kovács, Mihály, et al.
Published: (2025)