The first attempts to use regular tree languages for program
verification can be found in research papers from the early 80's.
Since then, a long standing research activity has tried to improve
these first results to expand their applicability, improve their
verification power, or explore their theoretical limits. During those
40 years of research, this small community came up with many results
but very few applications to real verification problems. Verification
of cryptographic protocols being one of them. However, several recent
papers from the formal verification community suggest that new
applications may arise. A first application is the automatic
verification of real size higher-order functional programs. Another
application is the extension of SMT solvers with regular tree languages
techniques to automatize the verification of programs manipulating
Algebraic Data Types.