diff --git a/lisa/src/main/java/it/unive/lisa/analysis/CartesianProduct.java b/lisa/src/main/java/it/unive/lisa/analysis/CartesianProduct.java
new file mode 100644
index 000000000..3cfceb196
--- /dev/null
+++ b/lisa/src/main/java/it/unive/lisa/analysis/CartesianProduct.java
@@ -0,0 +1,15 @@
+package it.unive.lisa.analysis;
+
+import it.unive.lisa.symbolic.SymbolicExpression;
+import it.unive.lisa.symbolic.value.Identifier;
+
+public abstract class CartesianProduct<T1 extends SemanticDomain<T1, E, I>, T2 extends SemanticDomain<T2, E, I>, E extends SymbolicExpression, I extends Identifier> {
+
+	protected T1 left;
+	protected T2 right;
+
+	protected CartesianProduct(T1 left, T2 right) {
+		this.left = left;
+		this.right = right;
+	}
+}
diff --git a/lisa/src/main/java/it/unive/lisa/analysis/ValueCartesianProduct.java b/lisa/src/main/java/it/unive/lisa/analysis/ValueCartesianProduct.java
new file mode 100644
index 000000000..c77dab6ac
--- /dev/null
+++ b/lisa/src/main/java/it/unive/lisa/analysis/ValueCartesianProduct.java
@@ -0,0 +1,76 @@
+package it.unive.lisa.analysis;
+
+import it.unive.lisa.symbolic.value.Identifier;
+import it.unive.lisa.symbolic.value.ValueExpression;
+
+public class ValueCartesianProduct<T1 extends ValueDomain<T1>, T2 extends ValueDomain<T2>>
+		extends CartesianProduct<T1, T2, ValueExpression, Identifier>
+		implements ValueDomain<ValueCartesianProduct<T1, T2>> {
+
+	public ValueCartesianProduct(T1 left, T2 right) {
+		super(left, right);
+	}
+
+	@Override
+	public ValueCartesianProduct<T1, T2> assign(Identifier id, ValueExpression expression) throws SemanticException {
+		T1 newLeft = left.assign(id, expression);
+		T2 newRight = right.assign(id, expression);
+		return new ValueCartesianProduct<T1, T2>(newLeft, newRight);
+	}
+
+	@Override
+	public ValueCartesianProduct<T1, T2> smallStepSemantics(ValueExpression expression) throws SemanticException {
+		T1 newLeft = left.smallStepSemantics(expression);
+		T2 newRight = right.smallStepSemantics(expression);
+		return new ValueCartesianProduct<T1, T2>(newLeft, newRight);
+	}
+
+	@Override
+	public ValueCartesianProduct<T1, T2> assume(ValueExpression expression) throws SemanticException {
+		T1 newLeft = left.assume(expression);
+		T2 newRight = right.assume(expression);
+		return new ValueCartesianProduct<T1, T2>(newLeft, newRight);
+	}
+
+	@Override
+	public ValueCartesianProduct<T1, T2> forgetIdentifier(Identifier id) throws SemanticException {
+		T1 newLeft = left.forgetIdentifier(id);
+		T2 newRight = right.forgetIdentifier(id);
+		return new ValueCartesianProduct<T1, T2>(newLeft, newRight);
+	}
+
+	@Override
+	public Satisfiability satisfies(ValueExpression expression) throws SemanticException {
+		return left.satisfies(expression).and(right.satisfies(expression));
+	}
+
+	@Override
+	public String representation() {
+		return left.representation() + ", " + right.representation();
+	}
+
+	@Override
+	public ValueCartesianProduct<T1, T2> lub(ValueCartesianProduct<T1, T2> other) throws SemanticException {
+		return new ValueCartesianProduct<T1, T2>(left.lub(other.left), right.lub(other.right));
+	}
+
+	@Override
+	public ValueCartesianProduct<T1, T2> widening(ValueCartesianProduct<T1, T2> other) throws SemanticException {
+		return new ValueCartesianProduct<T1, T2>(left.widening(other.left), right.widening(other.right));
+	}
+
+	@Override
+	public boolean lessOrEqual(ValueCartesianProduct<T1, T2> other) throws SemanticException {
+		return left.lessOrEqual(other.left) && right.lessOrEqual(other.right);
+	}
+
+	@Override
+	public ValueCartesianProduct<T1, T2> top() {
+		return new ValueCartesianProduct<T1, T2>(left.top(), right.top());
+	}
+
+	@Override
+	public ValueCartesianProduct<T1, T2> bottom() {
+		return new ValueCartesianProduct<T1, T2>(left.bottom(), right.bottom());
+	}
+}
diff --git a/lisa/src/test/java/it/unive/lisa/test/imp/tutorial/ConstantPropagation.java b/lisa/src/test/java/it/unive/lisa/test/imp/tutorial/ConstantPropagation.java
new file mode 100644
index 000000000..08228f23a
--- /dev/null
+++ b/lisa/src/test/java/it/unive/lisa/test/imp/tutorial/ConstantPropagation.java
@@ -0,0 +1,224 @@
+package it.unive.lisa.test.imp.tutorial;
+
+import it.unive.lisa.analysis.SemanticDomain.Satisfiability;
+import it.unive.lisa.analysis.SemanticException;
+import it.unive.lisa.analysis.nonrelational.BaseNonRelationalValueDomain;
+import it.unive.lisa.cfg.type.Type;
+import it.unive.lisa.symbolic.value.BinaryOperator;
+import it.unive.lisa.symbolic.value.Constant;
+import it.unive.lisa.symbolic.value.Identifier;
+import it.unive.lisa.symbolic.value.TernaryOperator;
+import it.unive.lisa.symbolic.value.UnaryOperator;
+
+public class ConstantPropagation extends BaseNonRelationalValueDomain<ConstantPropagation> {
+
+	public static final ConstantPropagation TOP = new ConstantPropagation(true, false);
+
+	private static final ConstantPropagation BOTTOM = new ConstantPropagation(false, true);
+
+	private final boolean isTop, isBottom;
+
+	private final Integer value;
+
+	public ConstantPropagation() {
+		this(null, true, false);
+	}
+
+	private ConstantPropagation(Integer value, boolean isTop, boolean isBottom) {
+		this.value = value;
+		this.isTop = isTop;
+		this.isBottom = isBottom;
+	}
+
+	private ConstantPropagation(Integer value) {
+		this(value, false, false);
+	}
+
+	private ConstantPropagation(boolean isTop, boolean isBottom) {
+		this(null, isTop, isBottom);
+	}
+
+	@Override
+	public ConstantPropagation top() {
+		return TOP;
+	}
+
+	@Override
+	public boolean isTop() {
+		return isTop;
+	}
+
+	@Override
+	public ConstantPropagation bottom() {
+		return BOTTOM;
+	}
+
+	@Override
+	public boolean isBottom() {
+		return isBottom;
+	}
+
+	@Override
+	public String representation() {
+		return isTop() ? "Non-constant" : isBottom() ? "Bot" : value.toString();
+	}
+
+	@Override
+	protected ConstantPropagation evalNullConstant() {
+		return top();
+	}
+
+	@Override
+	protected ConstantPropagation evalNonNullConstant(Constant constant) {
+		if (constant.getValue() instanceof Integer)
+			return new ConstantPropagation((Integer) constant.getValue());
+		return top();
+	}
+
+	@Override
+	protected ConstantPropagation evalTypeConversion(Type type, ConstantPropagation arg) {
+		return top();
+	}
+
+	@Override
+	protected ConstantPropagation evalUnaryExpression(UnaryOperator operator, ConstantPropagation arg) {
+		switch (operator) {
+		case NUMERIC_NEG:
+			return new ConstantPropagation(0 - value);
+		case STRING_LENGTH:
+			return top();
+		default:
+			return top();
+		}
+	}
+
+	@Override
+	protected ConstantPropagation evalBinaryExpression(BinaryOperator operator, ConstantPropagation left,
+			ConstantPropagation right) {
+		switch (operator) {
+		case NUMERIC_ADD:
+			return new ConstantPropagation(left.value + right.value);
+		case NUMERIC_DIV:
+			if (left.value % right.value != 0)
+				return top();
+			else
+				return new ConstantPropagation(left.value / right.value);
+		case NUMERIC_MOD:
+			return new ConstantPropagation(left.value % right.value);
+		case NUMERIC_MUL:
+			return new ConstantPropagation(left.value * right.value);
+		case NUMERIC_SUB:
+			return new ConstantPropagation(left.value - right.value);
+		default:
+			return top();
+		}
+	}
+
+	@Override
+	protected ConstantPropagation evalTernaryExpression(TernaryOperator operator, ConstantPropagation left,
+			ConstantPropagation middle, ConstantPropagation right) {
+		return top();
+	}
+
+	@Override
+	protected ConstantPropagation lubAux(ConstantPropagation other) throws SemanticException {
+		return equals(other) ? other : top();
+	}
+
+	@Override
+	protected ConstantPropagation wideningAux(ConstantPropagation other) throws SemanticException {
+		return lubAux(other);
+	}
+
+	@Override
+	protected boolean lessOrEqualAux(ConstantPropagation other) throws SemanticException {
+		return value == other.value;
+	}
+
+	@Override
+	public int hashCode() {
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + (isBottom ? 1231 : 1237);
+		result = prime * result + (isTop ? 1231 : 1237);
+		result = prime * result + ((value == null) ? 0 : value.hashCode());
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj) {
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		ConstantPropagation other = (ConstantPropagation) obj;
+		if (isBottom != other.isBottom)
+			return false;
+		if (isTop != other.isTop)
+			return false;
+		if (value == null) {
+			if (other.value != null)
+				return false;
+		} else if (!value.equals(other.value))
+			return false;
+		return true;
+	}
+
+	@Override
+	protected Satisfiability satisfiesIdentifier(Identifier identifier) {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	protected Satisfiability satisfiesNullConstant() {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	protected Satisfiability satisfiesNonNullConstant(Constant constant) {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	protected Satisfiability satisfiesTypeConversion(Type type, ConstantPropagation right) {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	protected Satisfiability satisfiesUnaryExpression(UnaryOperator operator, ConstantPropagation arg) {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	protected Satisfiability satisfiesBinaryExpression(BinaryOperator operator, ConstantPropagation left,
+			ConstantPropagation right) {
+
+		if (left.isTop() || right.isTop())
+			return Satisfiability.UNKNOWN;
+
+		switch (operator) {
+		case COMPARISON_EQ:
+			return left.value == right.value ? Satisfiability.SATISFIED : Satisfiability.NOT_SATISFIED;
+		case COMPARISON_GE:
+			return left.value >= right.value ? Satisfiability.SATISFIED : Satisfiability.NOT_SATISFIED;
+		case COMPARISON_GT:
+			return left.value > right.value ? Satisfiability.SATISFIED : Satisfiability.NOT_SATISFIED;
+		case COMPARISON_LE:
+			return left.value <= right.value ? Satisfiability.SATISFIED : Satisfiability.NOT_SATISFIED;
+		case COMPARISON_LT:
+			return left.value < right.value ? Satisfiability.SATISFIED : Satisfiability.NOT_SATISFIED;
+		case COMPARISON_NE:
+			return left.value != right.value ? Satisfiability.SATISFIED : Satisfiability.NOT_SATISFIED;
+		default:
+			return Satisfiability.UNKNOWN;
+		}
+	}
+
+	@Override
+	protected Satisfiability satisfiesTernaryExpression(TernaryOperator operator, ConstantPropagation left,
+			ConstantPropagation middle, ConstantPropagation right) {
+		return Satisfiability.UNKNOWN;
+	}
+}
diff --git a/lisa/src/test/java/it/unive/lisa/test/imp/tutorial/Parity.java b/lisa/src/test/java/it/unive/lisa/test/imp/tutorial/Parity.java
new file mode 100644
index 000000000..f4b8d9d8f
--- /dev/null
+++ b/lisa/src/test/java/it/unive/lisa/test/imp/tutorial/Parity.java
@@ -0,0 +1,220 @@
+package it.unive.lisa.test.imp.tutorial;
+
+import it.unive.lisa.analysis.SemanticDomain.Satisfiability;
+import it.unive.lisa.analysis.SemanticException;
+import it.unive.lisa.analysis.nonrelational.BaseNonRelationalValueDomain;
+import it.unive.lisa.cfg.type.Type;
+import it.unive.lisa.symbolic.value.BinaryOperator;
+import it.unive.lisa.symbolic.value.Constant;
+import it.unive.lisa.symbolic.value.Identifier;
+import it.unive.lisa.symbolic.value.TernaryOperator;
+import it.unive.lisa.symbolic.value.UnaryOperator;
+
+public class Parity extends BaseNonRelationalValueDomain<Parity> {
+
+	private enum Values {
+		ODD,
+		EVEN,
+		TOP,
+		BOT
+	}
+
+	private final Values parity;
+
+	private Parity(Values parity) {
+		this.parity = parity;
+	}
+
+	public Parity() {
+		this(Values.TOP);
+	}
+
+	@Override
+	public Parity top() {
+		return new Parity(Values.TOP);
+	}
+
+	@Override
+	public boolean isTop() {
+		return getParity() == Values.TOP;
+	}
+
+	@Override
+	public boolean isBottom() {
+		return getParity() == Values.BOT;
+	}
+
+	@Override
+	public Parity bottom() {
+		return new Parity(Values.BOT);
+	}
+
+	@Override
+	public String representation() {
+		switch (parity) {
+		case BOT:
+			return "BOT";
+		case ODD:
+			return "Odd";
+		case EVEN:
+			return "Even";
+		default:
+			return "TOP";
+		}
+	}
+
+	public Values getParity() {
+		return parity;
+	}
+
+	@Override
+	protected Parity evalNullConstant() {
+		return top();
+	}
+
+	@Override
+	protected Parity evalNonNullConstant(Constant constant) {
+		if (constant.getValue() instanceof Integer) {
+			Integer i = (Integer) constant.getValue();
+			return i % 2 == 0 ? even() : odd();
+		}
+
+		return top();
+	}
+
+	private Parity odd() {
+		return new Parity(Values.ODD);
+	}
+
+	private Parity even() {
+		return new Parity(Values.EVEN);
+	}
+
+	private boolean isEven() {
+		return parity == Values.EVEN;
+	}
+
+	private boolean isOdd() {
+		return parity == Values.ODD;
+	}
+
+	@Override
+	protected Parity evalTypeConversion(Type type, Parity arg) {
+		return top();
+	}
+
+	@Override
+	protected Parity evalUnaryExpression(UnaryOperator operator, Parity arg) {
+		switch (operator) {
+		case NUMERIC_NEG:
+			return arg;
+		default:
+			return top();
+		}
+	}
+
+	@Override
+	protected Parity evalBinaryExpression(BinaryOperator operator, Parity left, Parity right) {
+
+		switch (operator) {
+		case NUMERIC_ADD:
+		case NUMERIC_SUB:
+			if (right.equals(left))
+				return even();
+			else
+				return odd();
+		case NUMERIC_MUL:
+			if (left.isEven() || right.isEven())
+				return even();
+			else
+				return odd();
+		case NUMERIC_DIV:
+			if (left.isOdd())
+				return right.isOdd() ? odd() : even();
+			else
+				return right.isOdd() ? even() : top();
+		case NUMERIC_MOD:
+			return top();
+		default:
+			return top();
+		}
+	}
+
+	@Override
+	protected Parity evalTernaryExpression(TernaryOperator operator, Parity left, Parity middle, Parity right) {
+		return top();
+	}
+
+	@Override
+	protected Parity lubAux(Parity other) throws SemanticException {
+		return equals(other) ? other : top();
+	}
+
+	@Override
+	protected Parity wideningAux(Parity other) throws SemanticException {
+		return lubAux(other);
+	}
+
+	@Override
+	protected boolean lessOrEqualAux(Parity other) throws SemanticException {
+		return equals(other);
+	}
+
+	@Override
+	protected Satisfiability satisfiesIdentifier(Identifier identifier) {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	protected Satisfiability satisfiesNullConstant() {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	protected Satisfiability satisfiesNonNullConstant(Constant constant) {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	protected Satisfiability satisfiesTypeConversion(Type type, Parity right) {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	protected Satisfiability satisfiesUnaryExpression(UnaryOperator operator, Parity arg) {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	protected Satisfiability satisfiesBinaryExpression(BinaryOperator operator, Parity left, Parity right) {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	protected Satisfiability satisfiesTernaryExpression(TernaryOperator operator, Parity left, Parity middle,
+			Parity right) {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	public int hashCode() {
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + ((parity == null) ? 0 : parity.hashCode());
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj) {
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		Parity other = (Parity) obj;
+		if (parity != other.parity)
+			return false;
+		return true;
+	}
+}
\ No newline at end of file
diff --git a/lisa/src/test/java/it/unive/lisa/test/imp/tutorial/ParityXSign.java b/lisa/src/test/java/it/unive/lisa/test/imp/tutorial/ParityXSign.java
new file mode 100644
index 000000000..80efe4355
--- /dev/null
+++ b/lisa/src/test/java/it/unive/lisa/test/imp/tutorial/ParityXSign.java
@@ -0,0 +1,20 @@
+package it.unive.lisa.test.imp.tutorial;
+
+import it.unive.lisa.analysis.ValueCartesianProduct;
+import it.unive.lisa.analysis.nonrelational.ValueEnvironment;
+import it.unive.lisa.symbolic.value.Identifier;
+
+public class ParityXSign extends ValueCartesianProduct<ValueEnvironment<Parity>, ValueEnvironment<Sign>> {
+
+	public ParityXSign() {
+		super(new ValueEnvironment<Parity>(new Parity()), new ValueEnvironment<Sign>(new Sign()));
+	}
+
+	@Override
+	public String representation() {
+		String result = "";
+		for (Identifier x : left.getKeys())
+			result += x + ": (" + left.getState(x) + ", " + right.getState(x) + ")";
+		return result;
+	}
+}
\ No newline at end of file
diff --git a/lisa/src/test/java/it/unive/lisa/test/imp/tutorial/Sign.java b/lisa/src/test/java/it/unive/lisa/test/imp/tutorial/Sign.java
new file mode 100644
index 000000000..1be8e40e3
--- /dev/null
+++ b/lisa/src/test/java/it/unive/lisa/test/imp/tutorial/Sign.java
@@ -0,0 +1,296 @@
+package it.unive.lisa.test.imp.tutorial;
+
+import it.unive.lisa.analysis.SemanticDomain.Satisfiability;
+import it.unive.lisa.analysis.SemanticException;
+import it.unive.lisa.analysis.nonrelational.BaseNonRelationalValueDomain;
+import it.unive.lisa.cfg.type.Type;
+import it.unive.lisa.symbolic.value.BinaryOperator;
+import it.unive.lisa.symbolic.value.Constant;
+import it.unive.lisa.symbolic.value.Identifier;
+import it.unive.lisa.symbolic.value.TernaryOperator;
+import it.unive.lisa.symbolic.value.UnaryOperator;
+
+public class Sign extends BaseNonRelationalValueDomain<Sign> {
+
+	private enum Values {
+		POS,
+		NEG,
+		ZERO,
+		TOP,
+		BOT
+	}
+
+	private final Values sign;
+
+	private Sign(Values sign) {
+		this.sign = sign;
+	}
+
+	public Sign() {
+		this(Values.TOP);
+	}
+
+	@Override
+	public Sign top() {
+		return new Sign(Values.TOP);
+	}
+
+	@Override
+	public boolean isTop() {
+		return getSign() == Values.TOP;
+	}
+
+	@Override
+	public boolean isBottom() {
+		return getSign() == Values.BOT;
+	}
+
+	@Override
+	public Sign bottom() {
+		return new Sign(Values.BOT);
+	}
+
+	@Override
+	public String representation() {
+		switch (sign) {
+		case BOT:
+			return "Bottom";
+		case NEG:
+			return "-";
+		case POS:
+			return "+";
+		case ZERO:
+			return "0";
+		default:
+			return "Unknown sign";
+		}
+	}
+
+	public Values getSign() {
+		return sign;
+	}
+
+	@Override
+	protected Sign evalNullConstant() {
+		return bottom();
+	}
+
+	@Override
+	protected Sign evalNonNullConstant(Constant constant) {
+		if (constant.getValue() instanceof Integer) {
+			Integer i = (Integer) constant.getValue();
+			return i == 0 ? zero() : i > 0 ? pos() : neg();
+		}
+
+		return top();
+	}
+
+	private Sign pos() {
+		return new Sign(Values.POS);
+	}
+
+	private Sign neg() {
+		return new Sign(Values.NEG);
+	}
+
+	private Sign zero() {
+		return new Sign(Values.ZERO);
+	}
+
+	private boolean isPositive() {
+		return sign == Values.POS;
+	}
+
+	private boolean isZero() {
+		return sign == Values.ZERO;
+	}
+
+	private boolean isNegative() {
+		return sign == Values.NEG;
+	}
+
+	private Sign opposite() {
+		if (isTop() || isBottom())
+			return this;
+		return isPositive() ? neg() : isNegative() ? pos() : zero();
+	}
+
+	@Override
+	protected Sign evalTypeConversion(Type type, Sign arg) {
+		return top();
+	}
+
+	@Override
+	protected Sign evalUnaryExpression(UnaryOperator operator, Sign arg) {
+		switch (operator) {
+		case NUMERIC_NEG:
+			if (arg.isPositive())
+				return neg();
+			else if (arg.isNegative())
+				return pos();
+			else if (arg.isZero())
+				return zero();
+			else
+				return top();
+		default:
+			return top();
+		}
+	}
+
+	@Override
+	protected Sign evalBinaryExpression(BinaryOperator operator, Sign left, Sign right) {
+		switch (operator) {
+		case NUMERIC_ADD:
+			if (left.isZero())
+				return right;
+			else if (right.isZero())
+				return left;
+			else if (left.equals(right))
+				return left;
+			else
+				return top();
+		case NUMERIC_SUB:
+			if (left.isZero())
+				return right.opposite();
+			else if (right.isZero())
+				return left.opposite();
+			else if (left.equals(right))
+				return top();
+			else
+				return left;
+		case NUMERIC_DIV:
+			if (right.isZero())
+				return bottom();
+			else if (left.isZero())
+				return zero();
+			else if (left.equals(right))
+				return top();
+		case NUMERIC_MOD:
+			return top();
+		case NUMERIC_MUL:
+			if (left.isZero() || right.isZero())
+				return zero();
+			else if (left.equals(right))
+				return pos();
+			else
+				return neg();
+		default:
+			return top();
+		}
+	}
+
+	@Override
+	protected Sign evalTernaryExpression(TernaryOperator operator, Sign left, Sign middle, Sign right) {
+		return top();
+	}
+
+	@Override
+	protected Sign lubAux(Sign other) throws SemanticException {
+		return equals(other) ? other : top();
+	}
+
+	@Override
+	protected Sign wideningAux(Sign other) throws SemanticException {
+		return lubAux(other);
+	}
+
+	@Override
+	protected boolean lessOrEqualAux(Sign other) throws SemanticException {
+		return equals(other);
+	}
+
+	@Override
+	public int hashCode() {
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + ((sign == null) ? 0 : sign.hashCode());
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj) {
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		Sign other = (Sign) obj;
+		if (sign != other.sign)
+			return false;
+		return true;
+	}
+
+	@Override
+	protected Satisfiability satisfiesIdentifier(Identifier identifier) {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	protected Satisfiability satisfiesNullConstant() {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	protected Satisfiability satisfiesNonNullConstant(Constant constant) {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	protected Satisfiability satisfiesTypeConversion(Type type, Sign right) {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	protected Satisfiability satisfiesUnaryExpression(UnaryOperator operator, Sign arg) {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	protected Satisfiability satisfiesBinaryExpression(BinaryOperator operator, Sign left, Sign right) {
+		if (left.isTop() || right.isTop())
+			return Satisfiability.UNKNOWN;
+
+		switch (operator) {
+		case COMPARISON_EQ:
+			return left.eq(right);
+		case COMPARISON_GE:
+			return left.eq(right).or(left.gt(right));
+		case COMPARISON_GT:
+			return left.gt(right);
+		case COMPARISON_LE: // e1 <= e2 same as !(e1 > e2)
+			return left.gt(right).negate();
+		case COMPARISON_LT: // e1 < e2 -> !(e1 >= e2) && !(e1 == e2)
+			return left.gt(right).negate().and(left.eq(right).negate());
+		case COMPARISON_NE:
+			return left.eq(right).negate();
+		default:
+			return Satisfiability.UNKNOWN;
+		}
+	}
+
+	private Satisfiability eq(Sign other) {
+		if (!this.equals(other))
+			return Satisfiability.NOT_SATISFIED;
+		else if (isZero())
+			return Satisfiability.SATISFIED;
+		else
+			return Satisfiability.UNKNOWN;
+	}
+
+	private Satisfiability gt(Sign other) {
+		if (this.equals(other))
+			return this.isZero() ? Satisfiability.NOT_SATISFIED : Satisfiability.UNKNOWN;
+		else if (this.isZero())
+			return other.isPositive() ? Satisfiability.NOT_SATISFIED : Satisfiability.SATISFIED;
+		else if (this.isPositive())
+			return Satisfiability.SATISFIED;
+		else
+			return Satisfiability.NOT_SATISFIED;
+	}
+
+	@Override
+	protected Satisfiability satisfiesTernaryExpression(TernaryOperator operator, Sign left, Sign middle, Sign right) {
+		return Satisfiability.UNKNOWN;
+	}
+}
\ No newline at end of file
diff --git a/lisa/src/test/java/it/unive/lisa/test/imp/tutorial/intervals/Interval.java b/lisa/src/test/java/it/unive/lisa/test/imp/tutorial/intervals/Interval.java
new file mode 100644
index 000000000..f3a1d1aff
--- /dev/null
+++ b/lisa/src/test/java/it/unive/lisa/test/imp/tutorial/intervals/Interval.java
@@ -0,0 +1,186 @@
+package it.unive.lisa.test.imp.tutorial.intervals;
+
+import it.unive.lisa.analysis.SemanticDomain.Satisfiability;
+import it.unive.lisa.analysis.SemanticException;
+import it.unive.lisa.analysis.nonrelational.BaseNonRelationalValueDomain;
+import it.unive.lisa.cfg.type.Type;
+import it.unive.lisa.symbolic.value.BinaryOperator;
+import it.unive.lisa.symbolic.value.Constant;
+import it.unive.lisa.symbolic.value.Identifier;
+import it.unive.lisa.symbolic.value.TernaryOperator;
+import it.unive.lisa.symbolic.value.UnaryOperator;
+
+public class Interval extends BaseNonRelationalValueDomain<Interval> {
+
+	private final Intv val;
+
+	private Interval(Intv val) {
+		this.val = val;
+	}
+
+	public Interval() {
+		this(Intv.mkTop());
+	}
+
+	@Override
+	public Interval top() {
+		return new Interval(Intv.mkTop());
+	}
+
+	@Override
+	public boolean isTop() {
+		return val.isTop();
+	}
+
+	@Override
+	public boolean isBottom() {
+		return val.isBottom();
+	}
+
+	@Override
+	public Interval bottom() {
+		return new Interval(Intv.mkBottom());
+	}
+
+	@Override
+	public String representation() {
+		return val.toString();
+	}
+
+	public Intv getInterval() {
+		return val;
+	}
+
+	@Override
+	protected Interval evalNullConstant() {
+		return top();
+	}
+
+	@Override
+	protected Interval evalNonNullConstant(Constant constant) {
+		if (constant.getValue() instanceof Integer)
+			return new Interval(new Intv((Integer) constant.getValue(), (Integer) constant.getValue()));
+
+		return top();
+	}
+
+	@Override
+	protected Interval evalTypeConversion(Type type, Interval arg) {
+		return top();
+	}
+
+	@Override
+	protected Interval evalUnaryExpression(UnaryOperator operator, Interval arg) {
+
+		switch (operator) {
+		case NUMERIC_NEG:
+			return new Interval(new Intv(0, null).mul(new Intv(-1, -1)));
+		case STRING_LENGTH:
+			return new Interval(new Intv(0, null));
+		default:
+			return top();
+		}
+	}
+
+	@Override
+	protected Interval evalBinaryExpression(BinaryOperator operator, Interval left, Interval right) {
+		if (left.isBottom() || right.isBottom())
+			return bottom();
+
+		switch (operator) {
+		case NUMERIC_ADD:
+			return new Interval(left.getInterval().plus(right.getInterval()));
+		case NUMERIC_SUB:
+			return new Interval(left.getInterval().diff(right.getInterval()));
+		case NUMERIC_MUL:
+			return new Interval(left.getInterval().mul(right.getInterval()));
+		case NUMERIC_DIV:
+			return new Interval(left.getInterval().div(right.getInterval()));
+		case NUMERIC_MOD:
+			return top();
+		default:
+			return top();
+		}
+	}
+
+	@Override
+	protected Interval evalTernaryExpression(TernaryOperator operator, Interval left, Interval middle, Interval right) {
+		return top();
+	}
+
+	@Override
+	protected Interval lubAux(Interval other) throws SemanticException {
+		return new Interval(getInterval().lub(other.getInterval()));
+	}
+
+	@Override
+	protected Interval wideningAux(Interval other) throws SemanticException {
+		return new Interval(getInterval().widening(other.getInterval()));
+	}
+
+	@Override
+	protected boolean lessOrEqualAux(Interval other) throws SemanticException {
+		return getInterval().lessOrEqual(other.getInterval());
+	}
+
+	@Override
+	protected Satisfiability satisfiesIdentifier(Identifier identifier) {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	protected Satisfiability satisfiesNullConstant() {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	protected Satisfiability satisfiesNonNullConstant(Constant constant) {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	protected Satisfiability satisfiesTypeConversion(Type type, Interval right) {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	protected Satisfiability satisfiesUnaryExpression(UnaryOperator operator, Interval arg) {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	protected Satisfiability satisfiesBinaryExpression(BinaryOperator operator, Interval left, Interval right) {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	protected Satisfiability satisfiesTernaryExpression(TernaryOperator operator, Interval left, Interval middle,
+			Interval right) {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	public int hashCode() {
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + ((val == null) ? 0 : val.hashCode());
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj) {
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		Interval other = (Interval) obj;
+		if (val == null) {
+			if (other.val != null)
+				return false;
+		} else if (!val.equals(other.val))
+			return false;
+		return true;
+	}
+}
\ No newline at end of file
diff --git a/lisa/src/test/java/it/unive/lisa/test/imp/tutorial/intervals/Intv.java b/lisa/src/test/java/it/unive/lisa/test/imp/tutorial/intervals/Intv.java
new file mode 100644
index 000000000..a1cb39b9f
--- /dev/null
+++ b/lisa/src/test/java/it/unive/lisa/test/imp/tutorial/intervals/Intv.java
@@ -0,0 +1,349 @@
+package it.unive.lisa.test.imp.tutorial.intervals;
+
+import java.util.SortedSet;
+import java.util.TreeSet;
+import java.util.concurrent.atomic.AtomicBoolean;
+
+public class Intv {
+
+	private static final Intv TOP = new Intv() {
+		@Override
+		public boolean equals(Object obj) {
+			return this == obj;
+		}
+
+		@Override
+		public int hashCode() {
+			return "TOP".hashCode();
+		}
+	};
+
+	private static final Intv BOTTOM = new Intv() {
+		@Override
+		public boolean equals(Object obj) {
+			return this == obj;
+		}
+
+		@Override
+		public int hashCode() {
+			return "BOTTOM".hashCode();
+		}
+
+		@Override
+		public String toString() {
+			return "BOTTOM";
+		}
+	};
+
+	private final Integer low;
+
+	private final Integer high;
+
+	private Intv() {
+		low = null;
+		high = null;
+	}
+
+	public Intv(Integer low, Integer high) {
+		this.low = low;
+		this.high = high;
+	}
+
+	public Integer getLow() {
+		return low;
+	}
+
+	public boolean lowIsMinusInfinity() {
+		return low == null;
+	}
+
+	public Integer getHigh() {
+		return high;
+	}
+
+	public static Intv mkTop() {
+		return TOP;
+	}
+
+	public static Intv mkBottom() {
+		return BOTTOM;
+	}
+
+	public boolean isTop() {
+		return this == TOP;
+	}
+
+	public boolean isBottom() {
+		return this == BOTTOM;
+	}
+
+	/**
+	 * Yields true if and only if the upper bound of this interval is +infinity.
+	 * 
+	 * @return true only if that condition holds
+	 */
+	public boolean highIsPlusInfinity() {
+		return high == null;
+	}
+
+	public Intv bottom() {
+		return getBottom();
+	}
+
+	/**
+	 * Yields the unique bottom element.
+	 * 
+	 * @return the bottom element
+	 */
+	public static Intv getBottom() {
+		return BOTTOM;
+	}
+
+	public Intv top() {
+		return getTop();
+	}
+
+	public static Intv getTop() {
+		return TOP;
+	}
+
+	protected Intv lub(Intv other) {
+		Integer newLow = lowIsMinusInfinity() || other.lowIsMinusInfinity() ? null : Math.min(low, other.low);
+		Integer newHigh = highIsPlusInfinity() || other.highIsPlusInfinity() ? null : Math.max(high, other.high);
+		return new Intv(newLow, newHigh);
+	}
+
+	protected Intv widening(Intv other) {
+		Integer newLow, newHigh;
+		if (other.highIsPlusInfinity() || (!highIsPlusInfinity() && other.high > high))
+			newHigh = null;
+		else
+			newHigh = other.high;
+
+		if (other.lowIsMinusInfinity() || (!lowIsMinusInfinity() && other.low < low))
+			newLow = null;
+		else
+			newLow = other.low;
+
+		return new Intv(newLow, newHigh);
+	}
+
+	@Override
+	public int hashCode() {
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + ((high == null) ? 0 : high.hashCode());
+		result = prime * result + ((low == null) ? 0 : low.hashCode());
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj) {
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		Intv other = (Intv) obj;
+		if (high == null) {
+			if (other.high != null)
+				return false;
+		} else if (!high.equals(other.high))
+			return false;
+		if (low == null) {
+			if (other.low != null)
+				return false;
+		} else if (!low.equals(other.low))
+			return false;
+		return true;
+	}
+
+	@Override
+	public String toString() {
+		return "[" + (lowIsMinusInfinity() ? "-Inf" : low) + ", " + (highIsPlusInfinity() ? "+Inf" : high) + "]";
+	}
+
+	public Intv plus(Intv other) {
+		Integer newLow, newHigh;
+
+		if (lowIsMinusInfinity() || other.lowIsMinusInfinity())
+			newLow = null;
+		else
+			newLow = low + other.low;
+
+		if (highIsPlusInfinity() || other.highIsPlusInfinity())
+			newHigh = null;
+		else
+			newHigh = high + other.high;
+
+		return new Intv(newLow, newHigh);
+	}
+
+	public Intv diff(Intv other) {
+		Integer newLow, newHigh;
+
+		if (other.highIsPlusInfinity() || lowIsMinusInfinity())
+			newLow = null;
+		else
+			newLow = low - other.high;
+
+		if (other.lowIsMinusInfinity() || highIsPlusInfinity())
+			newHigh = null;
+		else
+			newHigh = high - other.low;
+
+		return new Intv(newLow, newHigh);
+	}
+
+	public Intv mul(Intv other) {
+		// this = [l1, h1]
+		// other = [l2, h2]
+
+		SortedSet<Integer> boundSet = new TreeSet<>();
+		Integer l1 = low;
+		Integer h1 = high;
+		Integer l2 = other.low;
+		Integer h2 = other.high;
+
+		AtomicBoolean lowInf = new AtomicBoolean(false), highInf = new AtomicBoolean(false);
+
+		// l1 * l2
+		multiplyBounds(boundSet, l1, l2, lowInf, highInf);
+
+		// x1 * y2
+		multiplyBounds(boundSet, l1, h2, lowInf, highInf);
+
+		// x2 * y1
+		multiplyBounds(boundSet, h2, l2, lowInf, highInf);
+
+		// x2 * y2
+		multiplyBounds(boundSet, h1, h2, lowInf, highInf);
+
+		return new Intv(lowInf.get() ? null : boundSet.first(), highInf.get() ? null : boundSet.last());
+	}
+
+	public Intv div(Intv other) {
+		// this = [l1, h1]
+		// other = [l2, h2]
+
+		SortedSet<Integer> boundSet = new TreeSet<>();
+		Integer l1 = low;
+		Integer h1 = high;
+		Integer l2 = other.low;
+		Integer h2 = other.high;
+
+		AtomicBoolean lowInf = new AtomicBoolean(false), highInf = new AtomicBoolean(false);
+
+		// l1 / l2
+		divideBounds(boundSet, l1, l2, lowInf, highInf);
+
+		// x1 / y2
+		divideBounds(boundSet, l1, h2, lowInf, highInf);
+
+		// x2 / y1
+		divideBounds(boundSet, h2, l2, lowInf, highInf);
+
+		// x2 / y2
+		divideBounds(boundSet, h1, h2, lowInf, highInf);
+
+		return new Intv(lowInf.get() ? null : boundSet.first(), highInf.get() ? null : boundSet.last());
+	}
+
+	private void multiplyBounds(SortedSet<Integer> boundSet, Integer i, Integer j, AtomicBoolean lowInf,
+			AtomicBoolean highInf) {
+		if (i == null) {
+			if (j == null)
+				// -inf * -inf = +inf
+				highInf.set(true);
+			else {
+				if (j > 0)
+					// -inf * positive
+					lowInf.set(true);
+				else if (j < 0)
+					// -inf * negative
+					highInf.set(true);
+				else
+					boundSet.add(0);
+			}
+		} else if (j == null) {
+			if (i > 0)
+				// -inf * positive
+				lowInf.set(true);
+			else if (i < 0)
+				// -inf * negative
+				highInf.set(true);
+			else
+				boundSet.add(0);
+		} else
+			boundSet.add(i * j);
+	}
+
+	private void divideBounds(SortedSet<Integer> boundSet, Integer i, Integer j, AtomicBoolean lowInf,
+			AtomicBoolean highInf) {
+		if (i == null) {
+			if (j == null)
+				// -inf * -inf = +inf
+				highInf.set(true);
+			else {
+				if (j > 0)
+					// -inf * positive
+					lowInf.set(true);
+				else if (j < 0)
+					// -inf * negative
+					highInf.set(true);
+
+				// division by zero!
+			}
+		} else if (j == null) {
+			if (i > 0)
+				// -inf * positive
+				lowInf.set(true);
+			else if (i < 0)
+				// -inf * negative
+				highInf.set(true);
+			else
+				boundSet.add(0);
+		} else if (j != 0) {
+			boundSet.add((int) Math.ceil(i / (double) j));
+			boundSet.add((int) Math.floor(i / (double) j));
+		}
+		// division by zero!
+	}
+
+	public boolean lessOrEqual(Intv other) {
+		if (equals(other))
+			return true;
+		return lessOrEqualLow(low, other.low) && lessOrEqualHigh(high, other.high);
+	}
+
+	// l1 >= l2
+	private boolean lessOrEqualLow(Integer l1, Integer l2) {
+		if (l1 == null) {
+			if (l2 == null)
+				return true;
+			else
+				return false;
+		} else {
+			if (l2 == null)
+				return true;
+			else
+				return l1 >= l2;
+		}
+	}
+
+	// h1 <= h2
+	private boolean lessOrEqualHigh(Integer h1, Integer h2) {
+		if (h1 == null) {
+			if (h2 == null)
+				return true;
+			else
+				return false;
+		} else {
+			if (h2 == null)
+				return false;
+			else
+				return h1 <= h2;
+		}
+	}
+}
\ No newline at end of file