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

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

College of Engineering Awards

Illinois CS Faculty Recognized for Excellence in Research and Teaching by College of Engineering

April 15, 2019   Nahrstedt wins Drucker Eminent Faculty Award, Fleck the Rose Award for Teaching Excellence, and Smaragdis and Kumar the Dean’s Award for Excellence in Research.
Professor Gul Agha

Gul Agha Shares Research on Wireless Sensors Used to Monitor Bridges and Civil Infrastructure

March 27, 2019  

Illinois Innovators podcast -- Gul Agha, professor of computer science and Director of the Open Systems Laboratory at the University of Illinois, joins the program. His widely cited work, "Actors: A Model of Concurrent Computing in Distributed Systems," provided a basis for a number of research projects in concurrent programming. Actor frameworks have been used to program Twitter, LinkedIn, Facebook Chat, and more.

Runtime Verification founder and Illinois CS Professor Grigore Rosu

Meet The Illinois Startup Helping NASA And Boeing Detect Errors In Their Software

January 3, 2019  

ChicagoInno -- A startup born at the University of Illinois has built technology that identifies problems in a company’s software, and it’s helping some of the biggest players in aerospace, automotive and blockchain with their code. Professor Grigore Rosu's Runtime Verification has developed tools to improve the safety and reliability of software systems. 

Illinois CS Professor Gul Agha

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."
Tarnay Vardhan

Wired In: Tanay Vardhan

November 11, 2018  

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