MENU 
The area of Formal Methods and Automated Reasoning is concerned with developing and deploying mathematically-rigorous and algorithmically-efficient solutions to prove the correct behavior of complex hardware and software or to help developers diagnose and eliminate their bugs. When applicable, formal verification is more thorough than empirical testing and can, under given assumptions, provide independently-checkable proofs of correctness.
Topics studied include specification formalisms (propositional, first-order, and temporal logics), verification (model checking, automated theorem proving), program synthesis (reactive synthesis, sketching, supervisory control), satisfiability and satisfiability modulo theories. The work in this area is quite interdisciplinary with applications ranging from computing systems to cyber-physical systems, robotics, aerospace and automotive systems.
Formal methods research combines a wide variety of theoretical computer science topics like logics, formal languages, automata theory, computational complexity theory with algorithms and programming languages.