This article introduces a new numerical abstract domain for static analysis, extending the previous Difference-Bound Matrices (DBMs) to represent linear invariants of the form $(\pm x \pm y \leq c)$, where $x$ and $y$ are program variables and $c$ is a constant. The domain is designed to be efficient, with an $O(n^2)$ memory cost and $O(n^3)$ time complexity for common abstract operators. The paper focuses on efficient representations and graph-based algorithms, including a normal form algorithm for equivalence testing and a widening operator for computing least fixpoint approximations. The octagon abstract domain is particularly useful for analyzing programs with numerical variables, such as those involving division by zero, out-of-bound array access, and deadlock. The article also discusses the extension of DBMs to handle interval constraints and sum constraints, and provides practical results demonstrating the effectiveness of the domain in proving safety properties of programs.This article introduces a new numerical abstract domain for static analysis, extending the previous Difference-Bound Matrices (DBMs) to represent linear invariants of the form $(\pm x \pm y \leq c)$, where $x$ and $y$ are program variables and $c$ is a constant. The domain is designed to be efficient, with an $O(n^2)$ memory cost and $O(n^3)$ time complexity for common abstract operators. The paper focuses on efficient representations and graph-based algorithms, including a normal form algorithm for equivalence testing and a widening operator for computing least fixpoint approximations. The octagon abstract domain is particularly useful for analyzing programs with numerical variables, such as those involving division by zero, out-of-bound array access, and deadlock. The article also discusses the extension of DBMs to handle interval constraints and sum constraints, and provides practical results demonstrating the effectiveness of the domain in proving safety properties of programs.