A method of proving the invariance of linear inequalities for linear loops

DOI10.1007/s10559-014-9653-1zbMath1323.68381OpenAlexW2040292390MaRDI QIDQ2263332

M. S. Lvov

Publication date: 18 March 2015

Published in: Cybernetics and Systems Analysis (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10559-014-9653-1

zbMATH Keywords

static program analysisinvariant system of linear inequalitieslinear invariant of a loop

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Linear inequalities of matrices (15A39) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Analysis of linear definite iterative loops

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Nonlinear invariants for linear loops and eigenpolynomials of linear operators
• Discovery of invariant equalities in programs over data fields
• Computing polynomial program invariants
• Polynomial invariants for linear loops
• Non-linear loop invariant generation using Gröbner bases
• Precise interprocedural analysis through linear algebra
• Search for invariant linear relationships in programs
• Invariant inequalities in programs interpreted over an ordered field
• Iterative methods of program analysis
• Iterative methods of program analysis: Equalities and inequalities
• Automatic Generation of Polynomial Loop Invariants
• An axiomatic basis for computer programming