Reasoning Algebraically About P-Solvable Loops

DOI10.1007/978-3-540-78800-3_18zbMath1134.68600OpenAlexW1585981132MaRDI QIDQ5458331

Laura Kovács

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

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30)

Related Items

Symbol elimination and applications to parametric entailment problems, Algebra-Based Loop Analysis, From Polynomial Invariants to Linear Loops, Change-of-bases abstractions for non-linear hybrid systems, Solving invariant generation for unsolvable loops, Symbolic computation in automated program reasoning, Generating invariants for non-linear loops by linear algebraic methods, Aligator: A Mathematica Package for Invariant Generation (System Description), Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops, Termination of polynomial loops, Counterexample- and simulation-guided floating-point loop invariant synthesis, Algebra-based synthesis of loops and their invariants (invited paper), An Iterative Method for Generating Loop Invariants, Automatic proving or disproving equality loop invariants based on finite difference techniques, Endomorphisms for Non-trivial Non-linear Loop Invariant Generation, Discovering non-terminating inputs for multi-path polynomial programs, Automatic complexity analysis of integer programs via triangular weakly non-linear loops

Uses Software

• Aligator
• Mathematica
• Theorema
• fastZeil

Cites Work

• \textit{Theorema}: Towards computer-aided mathematical theory exploration
• A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
• A holonomic systems approach to special functions identities
• Affine relationships among variables of a program
• A \textit{Mathematica} version of Zeilberger's algorithm for proving binomial coefficient identities
• SumCracker: A package for manipulating symbolic sums and related objects
• Generating all polynomial invariants in simple loops
• Computing the algebraic relations of \(C\)-finite sequences and multisequences
• Non-linear loop invariant generation using Gröbner bases
• Decision procedure for indefinite hypergeometric summation
• The synthesis of loop predicates
• Interprocedurally Analyzing Polynomial Identities
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item