$\newcommand{\bigsqcap}{\mathop ⨅}$ There is an ever growing need to establish properties of a software by means of program analysis techniques. In order to get into the topic, we first need to talk about lattices. In order to talk about lattices, let’s recap partial orders. Partial Orders A pair $\left(D, \sqsubseteq\right)$ with $D\not=\emptyset$ and a reflexive, transitive, and antisymmetric relation $\sqsubseteq$ is a partial order. For example, the powerset of any set with $\subseteq$ is such a partial order.