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.

Strengths and Impact

There are several thrusts of research in our area, their common denominator being the harmony we keep between theory and system development. Compilers, compiler optimizations, and program transformation are traditional topics, but we approach them using novel techniques and tools, which not only get the job done but also do it with a high level of correctness confidence, sometimes even provably correctly. Parallel computing and models for concurrency are complex areas where we have unique expertise. Several of our faculty push conventional formal methods and verification into the realm of cyber-physical systems, which have both discrete and continuous behaviors, as well as into probabilistic and approximate models of computation. Software testing is one of our core strengths in software engineering; it is often the case that 10% or more of all the papers in top testing conferences are authored by Illinois faculty. In programming languages, we cover semantics and logics for program reasoning very well, proposing frameworks and foundations that are significantly better than the state-of-the-art.

Our research covers a broad spectrum, from foundationally advanced interactive theorem proving and category and type theory, to practical software engineering such as test selection and energy consumption. Security is also one of our strengths, being known for one of the most prominent attacker models in the security community, as well as for using modern programming language and formal methods and software engineering techniques to detect security flaws and improve system security. Importantly, we are actively investigating ideas and success stories from other areas, such as operating systems, numerical analysis, artificial intelligence, machine learning, and natural language processing, to propose innovative synergies between these fields and our area and specific scientific interests.


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

Neural Testing and Debugging, ML4Code Interpretability, Analysis and Testing of Autonomous Software Systems

Many-Task Computing and Workflows, Parallel and Distributed Computing, Sustainable and Open Research Science Software

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

Verification, Automated Reasoning, Autonomous Systems, Embedded Systems

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

Formal Verification of Software, Security, Cyber-Physical Systems, and Probabilistic Programs; Automata Theory; Logic 

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