Reasoning Algebraically About P-Solvable Loops
From MaRDI portal
Recommendations
- Invariant Generation for P-Solvable Loops with Assignments
- A complete invariant generation approach for P-solvable loops
- Aligator: A Mathematica Package for Invariant Generation (System Description)
- Automatic Generation of Polynomial Loop Invariants
- Generating all polynomial invariants in simple loops
Cites work
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- A \textit{Mathematica} version of Zeilberger's algorithm for proving binomial coefficient identities
- A holonomic systems approach to special functions identities
- A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
- Affine relationships among variables of a program
- Computing the algebraic relations of \(C\)-finite sequences and multisequences
- Decision procedure for indefinite hypergeometric summation
- Generating all polynomial invariants in simple loops
- scientific article; zbMATH DE number 3941661 (Why is no real title available?)
- scientific article; zbMATH DE number 3497890 (Why is no real title available?)
- scientific article; zbMATH DE number 3550181 (Why is no real title available?)
- scientific article; zbMATH DE number 3574936 (Why is no real title available?)
- scientific article; zbMATH DE number 400659 (Why is no real title available?)
- scientific article; zbMATH DE number 1052006 (Why is no real title available?)
- scientific article; zbMATH DE number 1948385 (Why is no real title available?)
- scientific article; zbMATH DE number 1973372 (Why is no real title available?)
- Interprocedurally Analyzing Polynomial Identities
- Non-linear loop invariant generation using Gröbner bases
- SumCracker: A package for manipulating symbolic sums and related objects
- The synthesis of loop predicates
Cited in
(31)- Aligator.jl -- a Julia package for loop invariant generation
- Automatic complexity analysis of integer programs via triangular weakly non-linear loops
- Termination of polynomial loops
- Counterexample- and simulation-guided floating-point loop invariant synthesis
- Algebra-based synthesis of loops and their invariants (invited paper)
- Discovering non-terminating inputs for multi-path polynomial programs
- Automatic proving or disproving equality loop invariants based on finite difference techniques
- Degree and dimension estimates for invariant ideals of P-solvable recurrences
- An iterative method for generating loop invariants
- Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
- A complete invariant generation approach for P-solvable loops
- Invariant Generation for P-Solvable Loops with Assignments
- Aligator: A Mathematica Package for Invariant Generation (System Description)
- Endomorphisms for Non-trivial Non-linear Loop Invariant Generation
- Algebra-Based Loop Analysis
- From Polynomial Invariants to Linear Loops
- Solving invariant generation for unsolvable loops
- Symbolic computation in automated program reasoning
- Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs
- Pattern-based approach to automation of deductive verification of process-oriented programs: patterns, lemmas and algorithms
- (Un)solvable loop analysis
- Termination of triangular polynomial loops
- Polynomial loops: beyond termination
- On strongest algebraic program invariants
- Algebraic tools for computing polynomial loop invariants
- Targeting completeness: automated complexity analysis of integer programs
- Algebraic and algorithmic methods for computing polynomial loop invariants
- On termination of polynomial programs with equality conditions
- Symbol elimination and applications to parametric entailment problems
- Change-of-bases abstractions for non-linear hybrid systems
- Generating invariants for non-linear loops by linear algebraic methods
This page was built for publication: Reasoning Algebraically About P-Solvable Loops
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5458331)
