THE DEEP CONNECTIONS between logic and automata theory have led to extensive applications in formal specification and verification of systems. In recent years, research has focused on extensibility of such techniques to infinite-state systems. This has led to developing theories of transformations, applications to verification of timed/recursive/concurrent/probabilistic systems, database theory, distributed algorithms, programs running under weak memory models and cryptographic protocols. Logic has also been the ground for foundational research, revisiting classical model theory from computational perspectives. This has led to results in Skolem Lowenheim theorems in the finite, synthesis of Boolean functions and Skolem functions, definability in first-order theories of graphs, algebraic characterizations, block products of algebraic structures, and decidable fragments of first-order modal logics.