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.
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.
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
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
CS professor Marinov wins Test of Time award at FSE 2024
- News
- July 23, 2024