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; HPVM and ApproxHPVM systems for compiling and approximating programs running on heterogeneous systems; K FrameworkProbfuzz, PSense, and AxProf systems for testing probabilistic and randomized computations; the first complete formalizations of C, Java, and Javascript; and regression testing techniques.

CS Faculty, Affiliate Faculty, and Their Research Interests

Vikram Adve Programming Languages, Compilers, Parallel Programming, Domain-Specific Languages, Automated Debugging, Formal Verification, Software Repositories
Gul Agha Models for Concurrent Computation; Parallel and Distributed Algorithms 
Mattox Beckman Parsers and Parser Generators, Clone Detection, Functional Programming and Type Classes, Matching Logic, Category Theory
Elsa Gunter Formal Methods, Programming Languages, Software Engineering, Semantics, Interactive Theorem Proving, Model Checking, Type Systems, Program Verification, Compiler Correctness
Darko Marinov Software Engineering, Software Testing
Jose Meseguer Formal Executable Specification and Verification, Software Architecture 
Andrew Miller, Electrical & Computer Engineering Design of Secure Decentralized Systems and Cryptocurrencies
Sasa Misailovic Program Optimization Systems, Probabilistic Programming, Approximate Computing Techniques
Sayan Mitra,
Electrical & Computer Engineering
Cyber-physical Systems, Formal Verification, Synthesis, Safe Autonomy
David Padua Program Analysis, Transformation, and Optimization 
Madhusudan Parthasarathy Formal Methods, Software Verification, Model Checking, Decidable Logics 
Lawrence Rauchwerger Languages for Parallel Computing, Run-Time Systems for Parallel Computing, Compilers for Domain Specific Parallel Languages
Grigore Rosu Software, Design, Semantics and Implementation of Programming Specification Languages 
Mahesh Viswanathan Model Checking, Logic, Cyberphysical Systems, Software, Security
Tao Xie Software Engineering, Software Testing, Program Analysis, Software Analytics 
Tianyin Xu Operating Systems, Cloud and Datacenter Systems, System Reliability and Resilience, Large-Scale System Management, Configuration Management, and Reliability Engineering

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

Programming Languages, Formal Methods, and Software Engineering Research News

Profs. Sheldon Jacobson, Klara Nahrstedt, and Tao Xie are among 443 people to be awarded the distinction of AAAS Fellow this year.

Jacobson, Nahrstedt, and Xie Among Eight 2019 AAAS Fellows From Illinois

December 2, 2019   Profs. Sheldon Jacobson, Klara Nahrstedt, and Tao Xie are among 443 people to be awarded the distinction of AAAS Fellow this year.
Five accomplished Illinois Computer Science master’s students have been recognized for their academic achievements and leadership.

Meet the Siebel Scholars Class of 2020

October 2, 2019   Five accomplished Illinois Computer Science master’s students have been recognized for their academic achievements and leadership.
Prof. Sarita Adve was invited to share work done by the EPOCHS project, which is part of the $1.5 billion Electronics Resurgence Initiative.

Adve Presents Heterogeneous Systems Research at DARPA ERI Summit

September 18, 2019   Prof. Sarita Adve was invited to share work done by the EPOCHS project, which is part of the $1.5 billion Electronics Resurgence Initiative.
Assistant Professor Sasa Misailovic

Misailovic Wins NSF CAREER Award to Develop Tools to Improve Applications That Rely on Noisy Data

May 13, 2019   Misailovic plans to investigate whether the foundation for handling noisy data can be built on static program analysis, and to develop related coursework.
Brave co-founder and CEO Brendan Eich

The Brave Browser Launches Ads that Reward Users for Viewing

April 24, 2019  

TechCrunch -- With the latest desktop version of the Brave browser, users can now opt-in to the Brave Ads program. Brave is an ad-blocking web browser startup led by Brendan Eich (MS CS '86), creator of the JavaScript programming language and former Mozilla CEO. He’s long maintained that the vision is “bigger than an ad blocker.”