Inference of Polynomial Invariants for Imperative Programs: A Farewell to Gröbner Bases
No abstract available.
Related papers
- Non-linear loop invariant generation using Gröbner bases POPL 2004
- Extracting Linear Relations from Gröbner Bases for Formal Verification of And-Inverter Graphs TACAS 2025
- Isomorphisms of generic recursive polynomial types POPL 2004
- Simple Linear Loops: Algebraic Invariants and Applications POPL 2025
- AMulet 2.0 for Verifying Multiplier Circuits TACAS 2021
- Reasoning Algebraically About P-Solvable Loops TACAS 2008
- Complexity and information in invariant inference POPL 2020
- Learning the boundary of inductive invariants POPL 2021