The crux of Savitch's Theorem
A program running in space $f(n)$ can take up to $2^{O(f(n))}$ time (the constant depends on the alphabet size). Hence, it could potentially make up to $2^{O(f(n))}$ non-deterministic choices. Naively, going over all of them requires that many steps. Savitch's theorem shows how this can be accomplished using only $O(f(n)^2)$ space. The idea is to use a recursive "meet in the middle" approach. Let an upper bound on the running time of the machine be $T$. The initial tape is the the state of the tape when the machine is started up. The final tape is the state of the tape at the end of the execution. We "guess" (i.e., go over all possibilities) the final tape, and try to verify that this final tape can be reached from the initial tape. At the first level of the recursion, we "guess" the contents $X$ of the tape at time $T/2$. We then recurse into two similar tasks:


Verify that $X$ can be reached in $T/2$ steps from the initial tape.
Verify that the final tape can be reached from $X$ in $T/2$ steps.


Each of these is solved by recursion. We can reuse the space of the first task when we execute the second task. The base of the recursion is when the number of steps is one, in which case we can verify the claim directly. If it checks out, great. Otherwise, we signal failure, and this signal prompts us to make the next guess (at the appropriate level of recursion).

Each level of the recursion requires storage space of size $f(n)$, and there are $\log T = O(f(n))$ levels, so the total space consumption is $O(f(n)^2)$.