The FICS research group focuses on the theoretical foundations for interacting and computing systems, using semantics, logic and automata to specify, reason about, and synthesize correct functional behaviors as well as constrained and optimal quantitative performance. The work spans from individual programs to communicating components and cyber-physical systems, addressing behavioral and logical equivalences, satisfiability, proof systems and synthesis. We explore the trade-offs between expressiveness, decidability, and complexity, aiming to establish rich mathematical frameworks that enable the sound specification, verification, and design of trustworthy computational systems.