# Program analysis for Turing machines

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.

• While this is interesting and related, it is related in the opposite way, showing things that are in cases most likely not specified by the poster. The cases the poster may be interested in would be more like quick (or at least not too slow) verifiable cases of primitive recursive functions. Sort of like software engineering for some TM's. Even so, a reference search would likely involve these papers, and they may be a good launch point. Gerhard "Maybe For Biological Computational Machines?" Paseman, 2017.08.09. – Gerhard Paseman Aug 9 '17 at 20:32