Proving $ \{ \langle D_1, ... ,D_K \rangle : \text{ where } D_i \text{ are DFAs and } {\bigcap}_{i=1}^k L(D_i) = \emptyset \} $ is NP-Hard
The language $L$ is in fact PSPACE-complete, so in particular it's both NP-hard and coNP-hard. Here is a quick sketch of the proof.

$L$ is in PSPACE. This part is easy. The intersection of the DFAs can be realized as a DFA with $n^n$ many states, hence if the intersection is non-empty, there must be a word of length $n^n$ accepted by all DFAs. Counting up to $n^n$ requires $O(n\log n)$ space, so there is an NPSPACE machine for $L$: the machine guesses a word of length at most $n^n$ and verifies (in parallel) that the word is accepted by all DFAs. Savitch's theorem shows that NPSPACE=PSPACE, so we're done.

$L$ is PSPACE-hard. The reduction is from TQBF, which is the problem, given a formula $\varphi(x_1,\ldots,x_n)$, to decide the truth value of $\psi = \exists x_1 \forall x_2 \exists x_3 \cdots \varphi(x_1,\ldots,x_n)$. Consider some iterative algorithm for evaluating $\psi$: it goes over all possible assignments of $x_1,\ldots,x_n$, and computes intermediate values of $Q x_i \bar{Q} x_{i+1} \cdots \varphi(y_1,\ldots,y_{i-1},x_i,\ldots,x_n)$ (where $Q \in \{\forall,\exists\}$). We can write this computation as one long string $w$. The computation can be verified locally: for example, if all we wanted is to verify that $w$ is a $\#$-separated list of all numbers from $0$ to $2^n-1$ in binary (i.e. for $n=2$, $\#00\#01\#10\#11$), then we can write several regular expressions which verify this:


$w$ is a $\#$-separated list: $(\#(0+1)^n)^*$
$w$ starts with $0^n$: $\#0^n\Sigma^*$
$w$ ends with $1^n$: $\Sigma^*\#1^n$
The LSBs in $w$ behaves correctly: $(\#(0+1)^{n-1}0\#(0+1)^{n-1}1)^*$
The MSBs in $w$ behaves correctly: $(\sum_{i=0}^{n-2} \#0(0+1)^i0(0+1)^{n-2-i})^*\#01^{n-1}\#10^{n-1}(\#1(0+1)^{n-1})^*$
Similar (but more complicated) regular expression ensure that the other bits behave correctly.


All these expressions (and the corresponding DFAs!) are of length polynomial in $n$, and there is a polynomial number of them, so using DFA intersection you can express the fact that $w$ is of the given form.

The actual $w$ is more complicated, but the idea is the same. At the very end of $w$ will appear the actual value of $\psi$, and we can add a regular expression which verifies that $\psi$ is true. This reduces TQBF to DFA intersection.

The classical reference is Kozen's Lower bounds for natural proof systems, or you can check my account (Section 4) which proves a different result but contains everything that you need to prove that $L$ is PSPACE-hard.