Model-based projection (MBP) is a technique for approximate quantifier elimination, which is useful in cases when computing the exact quantifier elimination is too computationally expensive. MBP is used in several modern algorithms for property directed reachability of transition systems or for checking satisfiability of quantified formulas. The goal of this thesis is to improve MBP computation by using a recently introduced concept of invertibility conditions. The student will study the theoretical background and design an unifying framework for computing MBP that incorporates invertibility conditions. The student will also implement the algorithm for the theory of bit-vectors and evaluate its effectiveness on a suitable set of benchmarks.