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
| Andrew Miller, Electrical & Computer Engineering | design of secure decentralized systems and cryptocurrencies |
| 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
Subscribe to FM seminar mailing list
Programming Languages, Formal Methods, and Software Engineering Research News
Illinois CS Professor Gul Agha Named ACM Fellow
December 6, 2018 CS Professor Gul Agha has been named an ACM Fellow for “research in concurrent programming and formal methods."
Wired In: Tanay Vardhan
November 11, 2018The News-Gazette -- The News-Gazette's regular Wired-In feature focuses on Tanay Vardhan, a University of Illinois senior majoring in aerospace engineering who is also an Illinois Computer Science minor. "He's passionate about web development and working on a startup called Turkbox."
Sarita Adve Named Recipient of the ACM-IEEE CS Ken Kennedy Award
October 31, 2018HPCWire -- The Association for Computing Machinery and IEEE Computer Society have named Sarita Adve as the recipient of the 2018 ACM-IEEE CS Ken Kennedy Award. Also covered by CRA Bulletin.
Marinov Leads Team Trying to Speed Up, Improve Reliability of Continuous Integration
October 1, 2018 Continuous integration is an increasingly important part of software creation, but developers are limited by its speed and reliability. Professor Darko Marinov is trying to change that.
The Security Risks Of Smart Contracts
August 24, 2018Computing -- Blockchain-based smart contracts present a unique risk, and companies should be wary of deploying them, according to CS Professor Grigore Rosu. "There are two big problems ... The code is public so you can work out how to attack it. Secondly, once you have a smart contract - that's it. It deploys and you cannot change it."