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

Yuri Gurevich

Website

Manos Kapritsos

WebsiteMentoring Plan

Yatin Manerkar

WebsiteMentoring Plan

Satish Narayanasamy

Website

Karem Sakallah

WebsiteMentoring Plan

Westley Weimer

WebsiteMentoring Plan

ECE Faculty

Stephane Lafortune

Website

Necmiye Ozay

Website

Affiliated Faculty

Jean-Baptiste Jeannin

Website