Dedukti is a type-checker for the λΠ-calculus modulo theory, which has the particularity to allow the user to declare rewrite rules, especially in order to encode the logic he/she wants to use. Thanks to the Curry-Howard-De Bruijn correspondence, the type checking done by Dedukti can be used to check proofs. Unfortunately, to decide the type-checking, Dedukti needs the system of rewrite rules declared by the user, together with β-reduction, to be confluent and terminating. An external tool already exists to check the confluence, but no automatic tool exists for the termination, which must be checked independently by hand, before using Dedukti. The subject of this report (and more widely of the internship) is to develop such a tool. A first part of it is dedicated to an algorithm of termination checking: the Size-Change Principle. After a brief introduction to Dedukti, the algorithm is explained and the results obtained by an implementation of it for Dedukti are presented. The second and longest part of this report is much more theoretic, since it presents reducibility candidates for the λΠ-calculus modulo theory. Those reducibility candidates can then be used together with the Size-Change Principle detailed in the first part, to check the termination of a rewrite rule system, as explained in [Wah07].