What technique is used to implement type checking for CoC?
May I have a reference to why η expansion is invalid for CoC?

It's not invalid. It's up to choice whether $\eta$-conversion for functions (or other types) is included. The original CoC paper seems to omit it, but as you see ATAPL includes it. I'm not certain, but $\eta$ may have been omitted from the original source because it was difficult to handle in the strong normalization arguments, back in the days. Nowadays normalization proofs are more likely to be based on NbE themselves, and have no issues with $\eta$-rules. Modern Coq definitely has $\eta$ for functions, and it is generally considered a highly useful basic feature.

The rules QA-NABS-1, QA-NABS-2 seem to be implementing η expansion for stuck terms? Why do these rules not describe NBE?

They do specify $\eta$ for functions. It's not really NbE though. ATAPL only describes how to compare weak head normal forms for conversion in an iterated fashion, it does not say how to efficiently compute to whnf. The essential part of NbE is the separation of syntax and values; this is missing from the ATAPL exposition.

Indeed, normalization by evaluation has a number of characteristics that make it only suitable for certain theories: it η-expands expressions as many times as possible

This is incorrect. NbE is not necessarily type-directed, and does not necessarily include $\eta$-expansion. If you look at QA-NABS-1, QA-NABS-2 and the other rules in ATAPL, they can be adapted to a conversion checking algorithm on NbE values, which is a) purely syntax-directed b) does not require $\eta$-expansion in evaluation c) decides $\eta$-conversion for functions.

Is there a name for the rules given in ATAPL to implement type checking for CoC? They seem ad-hoc to me, and I don't understand how I would come up with them.

I'm not aware of any rigorous and generic way for specifying conversion checking algorithms. I would summarize the rules of thumbs as follows.
The specification of values is obtained from the specification of syntax by replacing binders with metalanguage functions or closures. Evaluation goes from syntax to values and performs $\beta$-reduction (but not necessarily $\eta$-conversions). Then, conversion checking can be implemented on values, proceeding purely structurally, except where we want syntax-directed $\eta$-checking in the manner specified in ATAPL.