How to prove if an algorithm is reentrant?
One approach is to design your code so it is "safe by construction", so re-entrant calls cannot happen.  For instance, one way to do this is to use mutual exclusion to ensure that your method can't be invoked again while it is in the middle of running, to ensure you'll never have two instances running at the same time.  For instance, this kind of approach is often used to ensure that interrupt handlers are correct: they often clear interrupts at the beginning and re-enable them at the end.

Another method is to take whatever code you already have and try to prove it will continue to function correctly even in the presence of re-entrant invocations.  Here you can pick your favorite formal logic for reasoning about program correctness.  For instance, you can use Hoare-style logic to specify the intended functionality and prove it correct.  Then, you consider a tweaked version of your code, where before and after each statement, there is a (non-deterministic) possibility of a recursive invocation of the method being externally invoked; now you prove that the tweaked version continues to meet the spec.  You can replace Hoare logic with any other method for program verification.