What is considered the state-of-the-art on program analysis (static and dynamic) for Turing machines? What references can I consult for this problem?
I am thinking of things like determining whether a state in the transition graph is reachable, which strings of consecutive symbols on the tape are possible or impossible, and so on. Of course, this is undecidable in general, but I'm looking for analyses that cover a wide range of cases.
This is a bit beyond what you are seeking, but nevertheless you might be interested in the work of Adam Yedidia and Scott Aaronson. They have constructed three different Turing machines, $G$, $R$, and $Z$, that have these properties:
$G$: Halts iff Goldbach's conjecture is false.
$R$: Halts iff the Riemann hypothesis is false.
$Z$: Cannot be proved in ZFC to not halt. If it halts, it proves ZFC is inconsistent. "$Z$ is a Turing machine for which the question of its behavior (whether or not it halts when run indefinitely) is equivalent to the consistency of ZFC."
Their work is intricately related to the Busy Beaver function, and certainly involves "state-of-the-art program analysis."
"A Relatively Small Turing Machine Whose Behavior Is Independent of Set Theory." arXiv:1605.04343. 2016.
"The 8000th Busy Beaver number eludes ZF set theory: new paper by Adam Yedidia and me." Scott Aaronson blog
Their appendix contains a precise description of the $7,918$-state TM $Z$, a snippet of which looks like this:
To attempt respond to the original intent of your question more directly,
"which strings of consecutive symbols on the tape are possible or impossible, and so on"
You probably know that:
(1) Finding a TM that accepts (say) all strings of exactly length $3$ is undecidable. This can be established via Rice's theorem.
(2) Detecting "dead code," i.e., unreachable states of a TM, is undecidable.
(3) Deciding whether a TM accepts any word at all, is undecidable.
