This project area includes our work on decidability, complexity, automata, regular theories, synthesis, and foundational questions in logic and verification.