Here's a result that gives some idea of how hard it is to characterise linear (let alone residually finite) groups of type $F$ (ie with a $K(G,1)$ that's a finite complex).

**Theorem:** There is a sequence of finite subsets $S_i\subseteq GL_{n_i}(\mathbb{Z})$ with the property that:

- for every $i$, either $G_i=\langle S_i\rangle$ is of type $F$ or $G_i$ is not finitely presentable (in particular not of type $F$);
- the set of $i$ such that $G_i$ is of type $F$ is recursively enumerable but not recursive.

So there is no algorithm to determine whether or not $G_i$ is of type $F$.

I can give details of the proof if anyone's interested. Basically, it's an easy application of the Haglund--Wise version of the Rips Construction.

**Details**

The first ingredient is a sequence of finite presentations for groups $(Q_i)$, with the property that the set $\{i\mid Q_i\cong 1\}$ is recursively enumerable but not recursive. We also want to set things up so the non-trivial $Q_i$ are infinite. Such sequences are quite well known, see for instance Chuck Miller's survey article.

The second ingredient is provided by Haglund and Wise, in one of many variations of a famous construction of Rips. For any finite presentation for a group $Q$, Haglund and Wise construct a short exact sequence

$1\to G\to \Gamma\to Q\to 1$

with the following properties:

- $\Gamma$ is the fundamental group of a `virtually special', non-positively curved square complex $X$; and
- $G$ is finitely generated.

Non-positive curvature is a local condition on $X$ which ensures that its universal cover is contractible; in particular, $\Gamma$ is of type $F$. Being `special' is a condition on the hyperplanes of $X$. All you need to know is that it ensures that $\Gamma$ is (virtually) a subgroup of a right-angled Coxeter group, from which it follows that $\Gamma$ is a subgroup of $GL_{n}(\mathbb{Z})$ for some $n$.

Everything in this construction is completely explicit. Given a presentation for $Q$, one can write down a presentation for $\Gamma$ and the generators $S$ for $G$. Furthermore, you can also write down an explicit embedding $\Gamma\hookrightarrow GL_n(\mathbb{Z})$.

Finally, we apply this construction to the $Q_i$. If $Q_i\cong 1$ then we have $G_i\cong\Gamma_i$, so in particular it's of type $F$. On the other hand, a result of Bieri ensures that if $Q_i$ is infinite then $G_i$ isn't finitely presentable. (This uses the fact that the $\Gamma_i$ are of cohomological dimension two.)