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: 1. 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$); 2. 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][1]. The second ingredient is provided by [Haglund and Wise][2], 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: 1. $\Gamma$ is the fundamental group of a `virtually special', non-positively curved square complex $X$; and 2. $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][3] 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.) [1]: http://www.ms.unimelb.edu.au/~cfm/papers/paperpdfs/msri_survey.all.pdf [2]: http://www.ams.org/mathscinet/search/publdoc.html?arg3=&co4=AND&co5=AND&co6=AND&co7=AND&dr=all&pg4=AUCN&pg5=AUCN&pg6=PC&pg7=ALLF&pg8=ET&review_format=html&s4=haglund&s5=wise&s6=&s7=&s8=All&vfpref=html&yearRangeFirst=&yearRangeSecond=&yrop=eq&r=2&mx-pid=2377497 [3]: http://www.ams.org/mathscinet/search/publdoc.html?arg3=&co4=AND&co5=AND&co6=AND&co7=AND&dr=all&pg4=AUCN&pg5=AUCN&pg6=PC&pg7=ALLF&pg8=ET&review_format=html&s4=bieri%252C%2520r*&s5=&s6=&s7=&s8=All&vfpref=html&yearRangeFirst=&yearRangeSecond=&yrop=eq&r=32&mx-pid=511782