Formal Methods

Vikram Adve

Professor Adve's broad research interest lies in using compilers (more generally, program analysis and transformation techniques) as tools for improving the performance, programmability, and security of modern computer systems. His research emphasizes the development of novel systems, compilation techniques, and (where necessary) language features to address these problems.
Gul Agha

The goal of Prof. Agha's research is to understand the nature of concurrent computation. Results of the research will lead to new ways to build and maintain open distributed systems. Specifically, his group is developing concurrent programming languages and systems that support applications with high-performance, fault-tolerance, or real-time requirements.
Elsa L. Gunter

The focus of Prof. Gunter's research has been and continues to be on theorem proving with an automated assistant, and its application to reasoning about protocols, programs, and programming language semantics. Theorem provers capable of supporting general mathematical reasoning offer the greatest flexibility for developing programming language semantics and for proving properties of programs.
Carl A. Gunter

Professor Gunter uses his background in programming languages to analyze protocols and systems with respect to trustworthy operation. Information about Professor Gunter's recent work is outlined on the Security Lab page.
Jingwei Huang

Dr. Huang's research in ITI focuses on (1) formal theories of trust, including the formal semantics of trust, measurement of uncertainty in trust, logics of trust, calculus of trust, trust evolution, and trust mechanisms; and (2) applications of formal trust models in distributed computing and open networks, such as trust in identity management and trust in social networks.
Kenneth J. Keefe

Ken Keefe is currently interested in model-based system validation of dependability/performance/security properties, and multi-formalism and multi-solution modeling frameworks. He is the principal developer and software architect for the Möbius modeling and simulation tool.
José Meseguer

Professor Meseguer is turning his formal method techniques towards analysis of security protocols and development of robust internetworking techniques in disruptive environments.
Madhusudan Parthasarathy

Professor Parthasarathy applies formal methods to the development of trustworthy software. The Java Interface Synthesis Tool (JIST) is an example of that work. JIST is a set of automated tools and techniques to synthesize interfaces to Java modules.
Grigore Rosu

Professor Rosu is interested in software in a broad sense. He has worked on the following subjects.
Scalable Formal Methods for Multidimensional Components

funded by the National Science Foundation