I will describe, in theory and by demonstrating explicit calculations in the system GAP, algorithms that for investigating infinite matrix groups through suitable congruence images. In an interplay of algorithms for matrix groups and algorithms for finitely presented groups it is possible to prove arithmeticity of certain subgroups (and to prove infinite index if we are lucky).