Parametric systems of linear congruences

Based on an extended quantifier elimination procedure for discretely valued fields, we devise algorithms for solving multivariate systems of linear congruences over the integers. This includes determining integer solutions for sets of moduli which are all power of a fixed prime, uniform p-adic integer solutions for parametric prime power moduli, lifting strategies for these uniform p-adic solutions for given primes, and simultaneous lifting strategies for finite sets of primes. The method is finally extended to arbitrary moduli.