Programming Languages, Formal Methods, and Software Engineering

The growing complexity and scale of software poses formidable challenges for reliability, security, performance, and productivity. Our faculty tackle these problems by developing innovative techniques in programming language design and semantics; techniques and tools for formal verification, software testing, and automated debugging; and models and verification techniques for embedded systems that interact with physical entities.

We are known for theoretical advances such as the Actor model of concurrencyrewriting logic and related semantic frameworks; concolic testing for automated test generation; automated logic reasoning; automated inference of specifications and invariants; and control-theoretic techniques for analyzing cyberphysical systems. We have also produced widely-used tools and techniques like the Maude rewriting engine; the LLVM compiler infrastructureHPVM and ApproxHPVM systems for compiling and approximating programs running on heterogeneous systems; K FrameworkProbfuzzPSense, and AxProf systems for testing probabilistic and randomized computations; the first complete formalizations of C, Java, and Javascript; and regression testing techniques.

Faculty & Affiliate Faculty

Programming Languages, Compilers, Parallel Programming, Domain-Specific Languages, Automated Debugging, Formal Verification, Software Repositories

Models for Concurrent Computation; Parallel and Distributed Algorithms 

Parsers and Parser Generators, Clone Detection, Functional Programming and Type Classes, Matching Logic, Category Theory

Formal Methods, Programming Languages, Software Engineering, Semantics, Interactive Theorem Proving, Model Checking, Type Systems, Program Verification, Compiler Correctness

Software Testing and Analysis, Mobile Apps Energy and Security Assessment, Machine Learning for Software Engineering, Search-Based Software Engineering

 Software Engineering, Software Testing

 Formal Executable Specification and Verification, Software Architecture 

Design of Secure Decentralized Systems and Cryptocurrencies

Program Optimization Systems, Probabilistic Programming, Approximate Computing Techniques

Formal Methods, Automated Reasoning 

Program Analysis, Transformation, and Optimization 

Formal Software Verification, Secure System Design, Program Synthesis, Logic, and AI

Languages for Parallel Computing, Run-Time Systems for Parallel Computing, Compilers for Domain Specific Parallel Languages

Proof Engineering, Proof Automation, Interactive Theorem Proving, Verification, Type Theory, and Dependent Types

Software, Design, Semantics and Implementation of Programming Specification Languages 

Numerical Program Analysis, Formal Verification, Abstract Interpretation, System Verification, Formal Automated Reasoning

Model Checking, Logic, Cyberphysical Systems, Software, Security

Software Engineering, Software Testing, Program Analysis, Software Analytics 

Operating Systems, Cloud and Datacenter Systems, System Reliability and Resilience, Large-Scale System Management, Configuration Management, Reliability Engineering

Software Engineering, Software Testing and Debugging, Automated Program Repair, Program Analysis, Synergy between AI/FM and Software Engineering

Adjunct Faculty

Software Engineering, General and Interactive Program Transformations 

Related News