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; the Chisel optimization system for approximate computing; the first complete formalizations of C, Java, and Javascript; regression test suite reduction techniques; and educational tools based on automated test generation (CodeHunt;Pex4Fun) that have attracted over a million users.
CS Faculty and Their Research Interests
| Vikram Adve | software security, programming models for heterogeneous platforms |
| Gul Agha | models for concurrent computation; parallel and distributed algorithms |
| Elsa Gunter | software engineering, programming languages, formal methods |
| Darko Marinov | software engineering, reliability & testing, theorem proving, model checking, rich specification languages |
| Jose Meseguer | formal executable specification and verification, software architecture |
| Sasa Misailovic | program optimization systems, approximate computing techniques |
| David Padua | program analysis, transformation, and optimization |
| Madhusudan Parthasarathy | formal methods, software verification, model checking, decidable logics |
| Grigore Rosu | software, design, semantics and implementation of programming specification languages |
| Mahesh Viswanathan | algorithmic verification of cyberphysical systems |
| Tao Xie | software engineering, software testing, program analysis, software analytics |
Affiliate Faculty
| Sayan Mitra, Electrical & Computer Engineering |
formal methods, automated reasoning |
Adjunct Faculty
| Danny Dig, EECS Department, Oregon State University | software engineering, general and interactive program transformations |
Programming Languages, Formal Methods, and Software Engineering Research Efforts and Groups
- PL/FM/SE at Illinois
- Coordinated Science Lab (CSL)
- Assured Cloud Computing-University Center of Excellence (ACC-UCoE) in the Information Trust Institute
- Science of Security (SOS) Lablet in the Information Trust Institute
- The LLVM Compiler Infrastructure
Seminars
Brett Daniel Software Engineering Seminar (cs591se), named in memory of Brett Daniel
https://wiki.cites.illinois.edu/wiki/display/SoftEng/Home
Programming Languages, Formal Methods, and Software Engineering Research News
Distinguished Lecture Series: Dr. Daniel Jackson
November 3, 2016 Dr. Daniel Jackson will discuss an evolving theory, based on the identification of concepts and purposes, to guide the design of software.
Rosu earns ASE Most Influential Paper award for work that helped launch runtime verification field
October 17, 2016 Rosu's 2001 paper bridged two seemingly different software engineering areas: testing and formal verification.
CS @ ILLINOIS Siebel Scholars Class of 2017
September 13, 2016 Meet the 2017 class of Siebel Scholars from CS @ ILLINOIS: Chamila Amithirigala, Spencer Gordon, Wenqi He, Dengfeng Li, and Vipul Venkataraman.
Xie recognized as Microsoft Research Outstanding Collaborator
August 22, 2016 CS Associate Professor and Willett Faculty Scholar Tao Xie was recently honored with a Microsoft Research Outstanding Collaborator Award.