Invariant inequalities in programs interpreted over an ordered field

DOI10.1007/BF01068351MaRDI QIDQ3777432zbMATH OpenFDO

Authors M. S. Lvov

Publication date 1986

Published in Cybernetics (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BF01068351

zbMATH Keywords

invariant relationspolynomial ringsfiniteness problemalgorithmically undecidablealgebra of dataapproximating sequences of idealsinvariant inequalitiesreal closure of a linearly ordered fieldU-Y model of programs

Mathematics Subject Classification ID

Polynomial rings and ideals; rings of integer-valued polynomials (13F20) Specification and verification (program logics, model checking, etc.) (68Q60) Fields related with sums of squares (formally real fields, Pythagorean fields, etc.) (12D15) Ordered fields (12J15)

Recommendations

• Publication:4729341
• scientific article; zbMATH DE number 3911682
• Discovery of invariant equalities in programs over data fields
• Invariants and well-foundedness in program algebra
• scientific article; zbMATH DE number 4131671
• scientific article; zbMATH DE number 3934388
• Order-invariant types and their applications
• scientific article; zbMATH DE number 806754
• Computing polynomial program invariants
• Generalizations of algorithms that find invariant relationships in programs over algebra of terms

Cites work

• Decision procedures for real and p‐adic fields

Cited in

(8)

• Iterative methods of program analysis: Equalities and inequalities
• Analysis of linear definite iterative loops
• scientific article; zbMATH DE number 4113989 (Why is no real title available?)
• Discovery of invariant equalities in programs over data fields
• scientific article; zbMATH DE number 4131671 (Why is no real title available?)
• scientific article; zbMATH DE number 3934388 (Why is no real title available?)
• A method of proving the invariance of linear inequalities for linear loops
• scientific article; zbMATH DE number 3911682 (Why is no real title available?)

This page was built for publication: Invariant inequalities in programs interpreted over an ordered field

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