Polynomial Invariants for Affine Programs
From MaRDI portal
Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10) Computational aspects of higher-dimensional varieties (14Q15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Symbolic computation and algebraic computation (68W30)
Abstract: We exhibit an algorithm to compute the strongest polynomial (or algebraic) invariants that hold at each location of a given affine program (i.e., a program having only non-deterministic (as opposed to conditional) branching and all of whose assignments are given by affine expressions). Our main tool is an algebraic result of independent interest: given a finite set of rational square matrices of the same dimension, we show how to compute the Zariski closure of the semigroup that they generate.
Recommendations
- Computing polynomial program invariants
- Polynomial invariants generation of programs
- Polynomial invariants by linear algebra
- Assigning invariant polynomials over polytopes
- Polynomial invariants for linear loops
- The structure of polynomial invariants of linear loops
- Computation of polytopic invariants for polynomial dynamical systems using linear programming
- Invariant sets for polynomials
- A rewriting technique for universal polynomial invariants
- scientific article; zbMATH DE number 1886607
Cited in
(33)- Intensional Kleene and Rice theorems for abstract program semantics
- Selectively-amortized resource bounding
- Algebra-based synthesis of loops and their invariants (invited paper)
- Lonely points in simplices
- The affine hull of a binary automaton is computable in polynomial time
- scientific article; zbMATH DE number 5564089 (Why is no real title available?)
- scientific article; zbMATH DE number 3911682 (Why is no real title available?)
- scientific article; zbMATH DE number 4113989 (Why is no real title available?)
- Toric varieties from cyclic matrix semigroups
- scientific article; zbMATH DE number 7559486 (Why is no real title available?)
- scientific article; zbMATH DE number 7559488 (Why is no real title available?)
- On Reachability Problems for Low-Dimensional Matrix Semigroups
- Automata, Languages and Programming
- Termination of linear loops under commutative updates
- From Polynomial Invariants to Linear Loops
- Solving invariant generation for unsolvable loops
- What else is undecidable about loops?
- Symbolic computation in automated program reasoning
- On the Monniaux problem in abstract interpretation
- Invariant relations for affine loops
- Quantum temporal logic and reachability problems of matrix semigroups
- Porous invariants for linear systems
- Semigroup intersection problems in the Heisenberg groups
- On the size of finite rational matrix semigroups
- Weighted basic parallel processes and combinatorial enumeration
- On the intersection problem for quantum finite automata
- The identity problem in the special affine group of \(\mathbb{Z}^2\)
- Determinisation and unambiguisation of polynomially-ambiguous rational weighted automata
- Algebraic tools for computing polynomial loop invariants
- A Rice's theorem for abstract semantics
- An abstract fixed-point theorem for Horn formula equations
- Algebraic and algorithmic methods for computing polynomial loop invariants
- Porous invariants
This page was built for publication: Polynomial Invariants for Affine Programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145329)
