Solving invariant generation for unsolvable loops
From MaRDI portal
Publication:6164420
DOI10.1007/978-3-031-22308-2_3zbMath1524.68070arXiv2206.06943MaRDI QIDQ6164420
George Kenison, Laura Kovács, Miroslav Stankovič, Marcel Moosbrugger, Daneshvar Amrollahi, Ezio Bartocci
Publication date: 28 July 2023
Published in: Static Analysis (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2206.06943
Related Items (1)
Cites Work
- Unnamed Item
- Unnamed Item
- The concrete tetrahedron. Symbolic sums, recurrence equations, generating functions, asymptotic estimates
- Aligator.jl -- a Julia package for loop invariant generation
- Polynomial invariants by linear algebra
- Analysis of Bayesian networks via prob-solvable loops
- Termination of polynomial loops
- Deductive proofs of almost sure persistence and recurrence properties
- Computing polynomial program invariants
- Generating all polynomial invariants in simple loops
- Computing the algebraic relations of \(C\)-finite sequences and multisequences
- Weakest Precondition Reasoning for Expected Run–Times of Probabilistic Programs
- Parallelotope Bundles for Polynomial Reachability
- Invariant Generation for Multi-Path Loops with Polynomial Assignments
- Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
- Logical analysis of programs
- Automatic Generation of Polynomial Loop Invariants
- Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences
- Polynomial Invariants for Affine Programs
- Reasoning Algebraically About P-Solvable Loops
- An axiomatic basis for computer programming
This page was built for publication: Solving invariant generation for unsolvable loops
