The paper presents an automatic method for determining linear equality and inequality constraints among variables in a program. This method, based on abstract interpretation, is applied to static analysis to deduce assertions about the program's behavior without user-provided inductive hypotheses or human interaction. The authors demonstrate that their approach can automatically derive constraints for a sorting procedure, such as \( B = N \), \( 1 \leq B \leq N \), and \( 1 \leq B \leq N \), among others. The method generalizes classical data flow analysis techniques, allowing for the discovery of symbolic constants and common subexpressions. It also enables the determination of loop invariants and induction variables. The paper discusses the formal representation of linear constraints using convex polyhedra and provides algorithms for transforming these constraints based on elementary program constructs like assignments, tests, and junctions. Experimental results show the effectiveness of the method in determining constraints efficiently.The paper presents an automatic method for determining linear equality and inequality constraints among variables in a program. This method, based on abstract interpretation, is applied to static analysis to deduce assertions about the program's behavior without user-provided inductive hypotheses or human interaction. The authors demonstrate that their approach can automatically derive constraints for a sorting procedure, such as \( B = N \), \( 1 \leq B \leq N \), and \( 1 \leq B \leq N \), among others. The method generalizes classical data flow analysis techniques, allowing for the discovery of symbolic constants and common subexpressions. It also enables the determination of loop invariants and induction variables. The paper discusses the formal representation of linear constraints using convex polyhedra and provides algorithms for transforming these constraints based on elementary program constructs like assignments, tests, and junctions. Experimental results show the effectiveness of the method in determining constraints efficiently.