Invariant Generation for Multi-Path Loops with Polynomial Assignments

DOI10.1007/978-3-319-73721-8_11zbMath1446.68031arXiv1801.03967OpenAlexW2781303448MaRDI QIDQ3296330

Maximilian Jaroschek, Andreas Humenberger, Laura Kovács

Publication date: 7 July 2020

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (8)

Algebra-Based Loop Analysis ⋮ Logic for reasoning about bugs in loops over data sequences (IFIL) ⋮ From Polynomial Invariants to Linear Loops ⋮ Solving invariant generation for unsolvable loops ⋮ What else is undecidable about loops? ⋮ Symbolic computation in automated program reasoning ⋮ Termination of polynomial loops ⋮ Algebra-based synthesis of loops and their invariants (invited paper)

Uses Software

• Aligator
• hyper
• RISCErgoSum

This page was built for publication: Invariant Generation for Multi-Path Loops with Polynomial Assignments