The field of formal verification and security is moving towards more efficient and automated methods for ensuring the correctness and security of complex systems. Researchers are exploring new approaches to verify tree-manipulating programs, procedural programs with integer arrays, and concurrent programs on weak memory models. Additionally, there is a growing interest in developing solvers for constrained Horn clauses and applying algebraic methods to define language-based security properties. Notable papers in this area include:

• Verifying Tree-Manipulating Programs via CHCs, which introduces a unified approach to verifying such programs using knitted-tree encoding and constrained Horn clauses.
• HornStr: A string Theory Solver for Constrained Horn Clauses, which presents the first solver for invariant synthesis for Regular Model Checking with string constraints. These developments have the potential to significantly advance the field of formal verification and security, enabling more efficient and automated methods for ensuring the correctness and security of complex systems.