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
WebsiteMentoring PlanImproving the functional correctness of digital integrated circuits, by developing technology that attacks the issue at design time, in post-silicon, and throughout the lifetime of a digital integrated component, in face of the challenges posed by fragile silicon and extreme design complexity.Peter M. Chen
WebsiteOperating systems, computer security, virtual machines, fault-tolerant computing.Yuri Gurevich
WebsiteQuantum computing, privacy and security, software engineering, and theoretical computer scienceRyan Huang
WebsiteMentoring PlanOperating systems, distributed systems, cloud and mobile computing, software dependability, program analysis.Manos Kapritsos
WebsiteMentoring PlanDistributed systems, fault tolerance, formal verification, transaction processing.Yatin Manerkar
WebsiteMentoring PlanFormal methods (modeling, verification, and synthesis) for hardware and software, hardware security, memory consistency, cache coherence, concurrency, ethical AI.Satish Narayanasamy
WebsiteMentoring PlanComputer Architecture; Program Analysis; Confidential Computing; Health SystemsCyrus Omar
WebsiteMentoring PlanFundamentally improving the programming experience for computational and data scientists, web app programmers, students and educators, and for people with disabilities who cannot effectively use
other programming tools.Karem A. Sakallah
WebsiteMentoring PlanComputer-aided design of electronic systems, Boolean satisfiability, discrete optimization, and hardware and software verification.Georgios Tzimpragos
WebsiteMentoring PlanComputer architecture, new models of computation, computing with emerging devicesXinyu Wang
WebsiteMentoring PlanProgramming Languages, Formal Methods, Software Engineering. Program synthesis, verification, analysis, and testing.Westley Weimer
WebsiteMentoring PlanProgramming languages; software engineering; medical imaging; program analysis, synthesis and improvement.ECE Faculty
Stéphane Lafortune
WebsiteSystem and control theory; Discrete event systems; Application to computer and communication systemsNecmiye Ozay
WebsiteComputational aspects of control system design; hybrid and cyber-physical systems; safe autonomy; system identification and validation; dynamics-based data analysis.Courtesy and Affiliated Faculty
MENU 
