This paper presents a method for automatically discovering linear constraints among variables in a program. The approach is based on abstract interpretation and is applied to determine linear equality or inequality relations among variables in a program. The method is demonstrated using a sorting algorithm, where linear constraints are derived automatically without user input or human interaction. These constraints provide information about the relationships between variables, such as bounds and dependencies. The paper discusses how classical data flow analysis techniques, such as constant propagation, can be understood as discovering simple linear equality relations. More complex relationships, such as symbolic constants and common subexpressions, can also be identified. The method is also applied to determine loop invariants and induction variables, which are not purely syntactic. The problem of determining equality relationships between a linear combination of variables and a constant was solved by Karr, who used an algorithm based on Wegbreit's work. However, this approach assumes that the properties to be discovered form a lattice with finite increasing chains, which is not valid for inequality relationships. The model of abstract interpretation proposed by Cousot is general enough to handle this problem. The paper describes the formal representations of linear constraints among variables, including the concept of a convex polyhedron and its frame. It also discusses the conversion between different representations of a polyhedron, such as between a system of linear inequalities and a frame representation. The paper then presents the transformation of linear assertions by elementary language constructs, including assignment, test nodes, and simple junction nodes. These transformations are based on the principles of abstract interpretation and are designed to correctly model the semantic properties of the program. The paper concludes with a discussion of the experimental implementation of the method, demonstrating its effectiveness in discovering linear constraints among variables in a program. The method is particularly useful for determining the validity of expressions within specified numeric or symbolic ranges, including compile-time overflow and array bound checking.This paper presents a method for automatically discovering linear constraints among variables in a program. The approach is based on abstract interpretation and is applied to determine linear equality or inequality relations among variables in a program. The method is demonstrated using a sorting algorithm, where linear constraints are derived automatically without user input or human interaction. These constraints provide information about the relationships between variables, such as bounds and dependencies. The paper discusses how classical data flow analysis techniques, such as constant propagation, can be understood as discovering simple linear equality relations. More complex relationships, such as symbolic constants and common subexpressions, can also be identified. The method is also applied to determine loop invariants and induction variables, which are not purely syntactic. The problem of determining equality relationships between a linear combination of variables and a constant was solved by Karr, who used an algorithm based on Wegbreit's work. However, this approach assumes that the properties to be discovered form a lattice with finite increasing chains, which is not valid for inequality relationships. The model of abstract interpretation proposed by Cousot is general enough to handle this problem. The paper describes the formal representations of linear constraints among variables, including the concept of a convex polyhedron and its frame. It also discusses the conversion between different representations of a polyhedron, such as between a system of linear inequalities and a frame representation. The paper then presents the transformation of linear assertions by elementary language constructs, including assignment, test nodes, and simple junction nodes. These transformations are based on the principles of abstract interpretation and are designed to correctly model the semantic properties of the program. The paper concludes with a discussion of the experimental implementation of the method, demonstrating its effectiveness in discovering linear constraints among variables in a program. The method is particularly useful for determining the validity of expressions within specified numeric or symbolic ranges, including compile-time overflow and array bound checking.