Invariant Generation for P-Solvable Loops with Assignments

DOI10.1007/978-3-540-79709-8_35MaRDI QIDQ3503653zbMATH OpenOpenAlexFDO

Authors Laura Kovács

Publication date 5 June 2008

Published in Computer Science – Theory and Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-79709-8_35

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30)

Recommendations

• Reasoning Algebraically About P-Solvable Loops
• A complete invariant generation approach for P-solvable loops
• Invariant generation for multi-path loops with polynomial assignments
• Aligator: A Mathematica Package for Invariant Generation (System Description)
• Polynomial invariants by linear algebra

Cited in

(13)

• Aligator.jl -- a Julia package for loop invariant generation
• Polynomial invariants by linear algebra
• Degree and dimension estimates for invariant ideals of P-solvable recurrences
• Invariant generation for multi-path loops with polynomial assignments
• Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
• A complete invariant generation approach for P-solvable loops
• Aligator: A Mathematica Package for Invariant Generation (System Description)
• Deciding properties of affine loops
• Synthesizing invariants by solving solvable loops
• Reasoning Algebraically About P-Solvable Loops
• Solving invariant generation for unsolvable loops
• D-finiteness: a success story
• Symbol elimination and applications to parametric entailment problems

Describes a project that uses

Uses Software

• Aligator
• SumCracker
• fastZeil
• Dependencies

This page was built for publication: Invariant Generation for P-Solvable Loops with Assignments

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3503653)