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 concurrency; rewriting 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 infrastructure; HPVM and ApproxHPVM systems for compiling and approximating programs running on heterogeneous systems; K Framework; Probfuzz, PSense, and AxProf systems for testing probabilistic and randomized computations; the first complete formalizations of C, Java, and Javascript; and regression testing techniques.
Relevant Seminars
- Brett Daniel Software Engineering Seminar (cs591se) Subscribe to FM seminar mailing list.
- Formal Methods Seminar (cs591fm) Subscribe to SE seminar mailing list.
- Illinois Computer Science Speaker Series: brings prominent leaders and experts to campus to share their ideas and promote conversations about important challenges and topics in the discipline.
Faculty & Affiliate Faculty
Automated Code Generation, Reliable Code Generation with LLMs
Partial Evaluation, Dependent Types, Category Theory
Formal Methods, Programming Languages, Software Engineering, Semantics, Interactive Theorem Proving, Model Checking, Type Systems, Program Verification, Compiler Correctness
Program analysis, testing, bug repair
Many-Task Computing and Workflows, Parallel and Distributed Computing, Sustainable and Open Research Science Software
Testing, Debugging, Coding Agents, LLM for Code, AI&SE, Vulnerability Detection
Software Engineering, Software Testing
Compiler Verification, Synthesis
Formal Executable Specification and Verification, Software Architecture
Design of Secure Decentralized Systems and Cryptocurrencies
Programming systems for AI-intensive applications: Languages, Compilers, Software engineering tools and Runtime systems.
Verification, Automated Reasoning, Autonomous Systems, Embedded Systems
Compilation, automatic refactoring, software verification, static and dynamic analysis
Formal verification, verification of AI systems, software verification, program synthesis
Parallel programming languages
Verification, Dependent Type Theory, Proof Automation, Proof Engineering, Programming Languages
Software, Design, Semantics and Implementation of Programming Specification Languages
Formal Methods, LLM Verification, Statistical Guarantees
Formal Verification of Software, Security, Cyber-Physical Systems, and Probabilistic Programs; Automata Theory; Logic
Software reliability
Software engineering