On strongest algebraic program invariants

DOI10.1145/3614319MaRDI QIDQ7031989zbMATH OpenFDO

Authors Ehud Hrushovski, Joël Ouaknine, Amaury Pouly, James Worrell

Publication date 5 February 2025

Published in Journal of the ACM (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1145/3614319

zbMATH Keywords

algebraic invariantsmatrix semigroupspolynomial programsprogram verificationZariski closure

Mathematics Subject Classification ID

Effectivity, complexity and computational aspects of algebraic geometry (14Q20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites work

• o-minimal invariants for linear loops
• A Gröbner-based treatment of elimination theory for affine varieties
• Affine relationships among variables of a program
• Automata, Languages and Programming
• Automatic generation of polynomial invariants of bounded degree using abstract interpretation
• Complete semialgebraic invariant synthesis for the Kannan-Lipton orbit problem
• Computing polynomial program invariants
• Computing the Galois group of a linear differential equation
• Decidability of the membership problem for \(2\times 2\) integer matrices
• Decidable and Undecidable Problems about Quantum Automata
• Discovering affine equalities using random interpretation
• Elements of mathematics: from Euclid to Gödel
• Elimination Techniques for Program Analysis
• Generating all polynomial invariants in simple loops
• scientific article; zbMATH DE number 435565 (Why is no real title available?)
• scientific article; zbMATH DE number 4071018 (Why is no real title available?)
• scientific article; zbMATH DE number 1223710 (Why is no real title available?)
• scientific article; zbMATH DE number 1226898 (Why is no real title available?)
• scientific article; zbMATH DE number 217454 (Why is no real title available?)
• scientific article; zbMATH DE number 871949 (Why is no real title available?)
• scientific article; zbMATH DE number 5194318 (Why is no real title available?)
• scientific article; zbMATH DE number 3056890 (Why is no real title available?)
• Inference of polynomial invariants for imperative programs: a farewell to Gröbner bases
• Introduction to feedback control
• Invariant generation for multi-path loops with polynomial assignments
• La finitude des représentations linéaires des semi-groupes est decidable
• Non-linear loop invariant generation using Gröbner bases
• On finite semigroups of matrices
• On the computation of the Zariski closure of finitely generated groups of matrices
• On the decidability of the existence of polyhedral invariants in transition systems
• Polynomial approximations of the relational semantics of imperative programs
• Polynomial invariants by linear algebra
• Quantum automata and algebraic groups
• Reasoning Algebraically About P-Solvable Loops
• Representation theory of finite monoids
• Semialgebraic invariant synthesis for the Kannan-Lipton orbit problem
• The complexity of local dimensions for constructible sets
• The octagon abstract domain
• Un algorithme calculant le cardinal, fini ou infini, des demi-groupes de matrices
• Unsolvability in 3 × 3 Matrices

Cited in

(8)

• Weighted basic parallel processes and combinatorial enumeration
• Linear loop synthesis for quadratic invariants
• On the intersection problem for quantum finite automata
• Slice closures of indexed languages and word equations with counting constraints
• Algebraic tools for computing polynomial loop invariants
• Minimizing cost register automata over a field
• An abstract fixed-point theorem for Horn formula equations
• Algebraic and algorithmic methods for computing polynomial loop invariants

This page was built for publication: On strongest algebraic program invariants

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