Available solvers for mixed integer programs (MIPs) focus on rapidly finding close to optimal solutions for feasible instances. The answers, however, are computed with finite precision, which might lead to wrong results. For most applications, the errors can be neglected. This situation changes fundamentally, if MIPs are used to study theoretical problems (i.e., a "computer proof" is needed), if feasibility questions are considered, and if wrong answers can have legal consequences. For such applications an exact MIP solver is required. The aim of this project is to develop such a solver.