Reasoning Algebraically About P-Solvable Loops
From MaRDI portal
Publication:5458331
DOI10.1007/978-3-540-78800-3_18zbMATH Open1134.68600OpenAlexW1585981132MaRDI QIDQ5458331FDOQ5458331
Publication date: 11 April 2008
Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-78800-3_18
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- SumCracker: A package for manipulating symbolic sums and related objects
- A \textit{Mathematica} version of Zeilberger's algorithm for proving binomial coefficient identities
- A holonomic systems approach to special functions identities
- Decision procedure for indefinite hypergeometric summation
- The synthesis of loop predicates
- Affine relationships among variables of a program
- Non-linear loop invariant generation using Gröbner bases
- Generating all polynomial invariants in simple loops
- A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- Interprocedurally Analyzing Polynomial Identities
- Computing the algebraic relations of \(C\)-finite sequences and multisequences
Cited In (18)
- Automatic complexity analysis of integer programs via triangular weakly non-linear loops
- Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
- Symbol elimination and applications to parametric entailment problems
- Discovering non-terminating inputs for multi-path polynomial programs
- Algebra-based synthesis of loops and their invariants (invited paper)
- Symbolic computation in automated program reasoning
- Aligator: A Mathematica Package for Invariant Generation (System Description)
- Counterexample- and simulation-guided floating-point loop invariant synthesis
- Termination of polynomial loops
- Endomorphisms for Non-trivial Non-linear Loop Invariant Generation
- From Polynomial Invariants to Linear Loops
- An Iterative Method for Generating Loop Invariants
- Change-of-bases abstractions for non-linear hybrid systems
- Generating invariants for non-linear loops by linear algebraic methods
- Algebra-Based Loop Analysis
- Automatic proving or disproving equality loop invariants based on finite difference techniques
- Solving invariant generation for unsolvable loops
- Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs
Uses Software
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)
