Home > Research > Research Areas > Formal Methods & Automated Reasoning

Formal Methods & Automated Reasoning

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.

CSE Faculty

Valeria Bertacco

Website

Peter Chen

Website

Yuri Gurevich

Website

Ryan Huang

Website

Manos Kapritsos

Website

Yatin Manerkar

Website

Satish Narayanasamy

Website

Cyrus Omar

Website

Karem Sakallah

Website

Georgios Tzimpragos

Website

Xinyu Wang

Website

Westley Weimer

Website

ECE Faculty

Stephane Lafortune

Website

Necmiye Ozay

Website

Affiliated Faculty

Jean-Baptiste Jeannin

Website