One of the approaches for formal program verification is to convert an unrestricted grammar G_1 into a context-sensitive grammar G_2 subject to some constraints C. We then derive a linear bounded automaton A_2 that accepts the language L(G_2). We then transform the input program i.e., a string S_1 in L(G_1) to a modified program i.e., a string S_2 in L(G_2). If A_2 halts on S_2 then A_1 halts on S_1. By definition, A_2 accepts S_2. Therefore, A_1 accepts S_1.

Of course, L(G_2) is a subset of L(G_1) which means that many programs written in G_1 that do not meet the constraints C cannot be verified. But the benefit is that programs that do meet the constraints C are provably verified.

The tension lies in keeping C small and maximizing utility of the approach for a wide class of programs/libraries/programming paradigms etc.,