Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences

DOI10.1145/3087604.3087623zbMath1457.68063arXiv1705.02863OpenAlexW3099373080MaRDI QIDQ5119943

Laura Kovács, Maximilian Jaroschek, Andreas Humenberger

Publication date: 9 September 2020

Published in: Proceedings of the 2017 ACM on International Symposium on Symbolic and Algebraic Computation (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1705.02863

zbMATH Keywords

recurrence relationsprogram analysisloop invariantshypergeometric sequences

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Numerical aspects of recurrence relations (65Q30)

Related Items (4)

Lonely points in simplices ⋮ Solving invariant generation for unsolvable loops ⋮ Symbolic computation in automated program reasoning ⋮ Algebra-based synthesis of loops and their invariants (invited paper)

Uses Software

• Aligator
• Mathematica
• hyper

This page was built for publication: Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences