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, joining fall 2016 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

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

Dr. Milos Gligoric (PhD CS '15)

Milos Gligoric Receives ACM SIGSOFT Dissertation Award

July 20, 2016   Milos Gligoric (PhD CS ’15) is the 2016 recipient of the ACM SIGSOFT Outstanding Doctoral Dissertation Award.
CS Professor Josep Torrellas

NSF funds research to advance scalability for on-chip wireless communications

July 5, 2016   CS researchers to receive $880,000 in NSF funding to to advance scalability for on-chip wireless communications.
vikram adve

Vikram Adve Named University Scholar

October 15, 2015   CS Professor Vikram Adve was one of seven Urbana campus faculty members selected as a 2015 University Scholar.
Mahesh Viswanathan

Research Combines Simulations and Static Analysis to Verify Cyberphysical Systems

November 20, 2014   Mahesh Viswanathan is part of a research team finding ways to verify cyberphysical system reliability.
Gul Agha

Upgrading Programming for Mobile Cloud

October 27, 2014   CS Professors Gul Agha and Darko Marinov propose a new methodology for building mobile cloud applications.