Programming Languages, Formal Methods, and Software Engineering

word cloud with programming-related wordsThe 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 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


Brett Daniel Software Engineering Seminar (cs591se), named in memory of Brett Daniel
Subscribe to FM seminar mailing list

Programming Languages, Formal Methods, and Software Engineering Research News

Illinois CS Professor Darko Marinov

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.
CS Professor Grigore Rosu

The Security Risks Of Smart Contracts

August 24, 2018  

Computing -- 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."

DARPA funding will support research to explore the development of flexible architectures capable of using specialized hardware to solve specific computing problems more quickly and efficiently.

Illinois CS Researchers Among Teams Selected by DARPA to Unleash Power of Specialized and Reconfigurable Hardware

July 28, 2018   Researchers will explore the development of flexible architectures capable of using specialized hardware to solve specific computing problems more quickly and efficiently.
CS Professor Grigore Rosu

The K Framework – A Framework To Formally Define All Programming Languages

June 12, 2018  

Epicenter podcast -- CS Professor Grigore Rosu talks about the K framework, as well as his work to create a new virtual machine called IELE specifically tailored to blockchain. 

CS Professor Grigore Rosu

Runtime Verification And IOHK Launch Virtual Machine for Blockchain

December 18, 2017  

Payments Journal -- On the new release by Runtime Verification, Professor Grigore Rosu’s startup, of IELE, its new virtual machine for the blockchain.